zbMATH — the first resource for mathematics

The power of proofs: new algorithms for timed automata model checking. (English) Zbl 1448.68297
Legay, Axel (ed.) et al., Formal modeling and analysis of timed systems. 12th international conference, FORMATS 2014, Florence, Italy, September 8–10, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8711, 115-129 (2014).
Summary: This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, \(L^{\mathrm{rel}, \mathrm{af}}_{\nu,\mu}\), and reports performance results for an implementation. This mu-calculus contains extended time-modality operators and can express all of TCTL. Our algorithmic approach uses an “on-the-fly” strategy based on proof search as a means of ensuring high performance for both positive and negative answers to model-checking questions. In particular, a set of proof rules for solving model-checking problems are given and proved sound and complete; our algorithm then model-checks a property by constructing a proof (or showing none exists) using these rules. One noteworthy aspect of our technique is that we show that verification performance can be improved with derived rules, whose correctness can be inferred from the more primitive rules on which they are based. In this paper, we give the basic proof rules underlying our method, describe derived proof rules to improve performance, and we compare our implementation to UPPAAL.
For the entire collection see [Zbl 1317.68012].
68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Full Text: DOI