Jeroen Keiren: Tableaux for mu-calculus model checking of infinite state systems: a note on soundness

Event Details

In 1992, Bradfield and Stirling presented a tableaux-based approach to local model checking of infinite-state systems that is sound and complete. When trying to apply this approach to model-checking timed and hybrid automata against mu-calculus properties we observed that the approach is not practical. In this talk I will explain Bradfield and Stirling’s proof system, and illustrate its limitations. I will then show how, at the cost of losing completeness, the proof system can be made more practical. Unfortunately, the modifications break the existing soundness proof. I therefore propose an alternative approach to the soundness proof that is more robust when varying with the proof rules and termination conditions.