A divide & conquer approach to liveness model checking under fairness & anti-fairness assumptions
- 15 Downloads
This paper proposes an approach to making liveness model checking problems under fairness feasible. The proposed method divides such a problem into smaller ones that can be conquered. It is not superior to existing tools dedicated to model checking liveness properties under fairness assumptions in terms of model checking performance but has the following positive aspects: 1) the approach can be used to model check liveness properties under anti-fairness assumptions as well as fairness assumptions, 2) the approach can help humans better understand the reason why they need to use fairness and/or anti-fairness assumptions, and 3) the approach makes it possible to use existing linear temporal logic model checkers to model check liveness properties under fairness and/or anti-fairness assumptions.
Keywordsanti-fairness fairness liveness property Maude model checking
Unable to display preview. Download preview PDF.
The author wishes to thank anonymous referees who commented on drafts of this article. This article was partially supported by JSPS Kakenhi (23220002, 26540024).
- 1.Ogata K, Zhang M. A divide & conquer approach to model checking of liveness properties. In: Proceedings of the 37th Annual IEEE Computer Software and Applications Conference. 2013, 648–657Google Scholar
- 2.Ogata K. Model checking liveness properties under fairness & antifairness assumptions. In: Proceedings of the 20th Asia-Pacific Software Engineering Conference. 2013, 565–570Google Scholar
- 4.Lamport L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., 2002Google Scholar
- 5.Clarke EM, Grumberg O, Peled D A. Model Checking. Massachusetts: MIT Press, 1999Google Scholar
- 6.Latvala T. Model checking LTL properties of high-level Petri nets with fairness constraints. In: Proceedings of the 22nd International Conference on Application and Theory of Petri Nets. 2001, 242–262Google Scholar
- 12.Holzmann G J. The SPIN Model Checker–Primer and Reference Manual. Reading: Addison-Wesley, 2004Google Scholar
- 21.McMillan K L. Applications of Craig interpolants in model checking. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 1–12Google Scholar
- 24.Clarke EM, Long D E, McMillan K L. Compositional model checking. In: Proceedings of the 4th Symposium on Logic in Computer Science. 1989, 353–362Google Scholar
- 26.Abadi M, Lamport L. Open systems in TLA. In: Proceedings of the 13th ACM Symposium on Principles of Distributed Computing. 1994, 81–90Google Scholar