AbstractWe present a local model checking algorithm that decides for a given context-free process whether it satisfies a property written in the alternation-free modal mu-calculus. Heart of this algorithm is a purely syntactical sound and complete formal system, which in contrast to the known tableaux techniques, uses intermediate second-order assertions. These assertions provide a finite representation of all the infinite state sets which may arise during the proof in terms of the finite representation of the context-free argument process. This is the key to the effectiveness of our local model checking procedure.
Categories and Subject Descriptors: F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; D.2.4 [Software Engineering]: Program Verification
Selected references
- Rance Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(8):725-747, 1989.