Abstract:
Vacuity arises when a logical formula is trivially true in a given model due, for example, to antecedent failure. Beer et al. have recently introduced a logic-independent notion of vacuity and shown that certain logics, i.e., those with with polarity, admit an efficient decision procedure for vacuity detection. We show that the modal mu-calculus, a very expressive temporal logic, is a logic with polarity and hence the results of Beer et al. are applicable. We also extend the definition of vacuity to achieve a new notion of redundancy in logical formulas. Redundancy captures several forms of antecedent failure that escape traditional vacuity analysis, including vacuous actions in temporal modalities and unnecessarily strong temporal operators. Furthermore, we have implemented an efficient redundancy checker for the modal mu-calculus in the context of the XMC model checker. Our checker generates diagnostic information in the form of all maximal subformulas that are vacuous and the contexts in which they occur; and exploits the fact that XMC can cache intermediate results in memo tables between model-checking runs. We have applied our redundancy checker to a number of previously published case studies, and found instances of vacuity that have gone unnoticed till now. These findings provide compelling evidence of the importance of redundancy detection in the design process.
Bibtex Entry:
@inproceedings{DRSS:AMAST02, author = {Yifei Dong and C. R. Ramakrishnan and Beata Sarna-Starosta and Scott A. Smolka}, title = {Vacuity Checking in the Modal Mu-Calculus}, booktitle = {Ninth International Conference on Algebric Methodology and Software Technology ({AMAST})}, address = {Reunion Island, France}, month = {September}, series = {Lecture Notes in Computer Science}, volume = {2422}, publisher = {Springer}, pages = {147--162}, year = {2002} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)