The Power of Proofs: New Algorithms for Timed Automata Model Checking (with Appendix)

Peter Fontana, Rance Cleaveland

This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L_{\nu ,\mu }^{rel,af}$, and reports performance resul…