Detection of vacuously true properties

A property is vacuously true if at least one part of the property is irrelevant to its truth value. For example, ”all blue men have three legs” is vacuously true if there is no blue man, hence, the property ”all blue men are X” is always true whatever X is. Formally, a logic statement is vacuously true if it remains true for arbi- trary replacements of a part of the statement. Detecting vacuity when verifying systems is useful as they typically correspond to misformulated properties or modelling errors. For typical logics, vacuity can be detected by checking state- ments where sub-parts have been replaced by true or false. In this thesis, we are going to introduce an Enhanced Model-Checker for CTL in system verification tools, which is especially used for vacuity checking, and which is based on the PyNuSMV framework.