Verify LTL with Fairness Assumptions Efficiently

Publisher:
IEEE
Publication Type:
Conference Proceeding
Citation:
Proceedings of the International Symposium on Temporal Representation and Reasoning (TIME), 2016, pp. 41 - 50
Issue Date:
2016-12-05
Full metadata record
Files in This Item:
Filename Description Size
VERIFY LTL-2062017.pdfAccepted Manuscript263.73 kB
Adobe PDF
© 2016 IEEE.This paper deals with model checking problems with respect to LTL properties under fairness assumptions. We first present an efficient algorithm to deal with a fragment of fairness assumptions and then extend the algorithm to handle arbitrary ones. Notably, by making use of some syntactic transformations, our algorithm avoids constructing corresponding Büchi automata for the whole fairness assumptions, which can be very large in practice. We implement our algorithm in NuSMV and consider a large selection of formulas. Our experiments show that in many cases our approach exceeds the automata-theoretic approach up to several orders of magnitude, in both time and memory.
Please use this identifier to cite or link to this item: