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

TL;DR

This paper introduces a novel model-checking algorithm for an expressive modal mu-calculus over timed automata, utilizing proof search and derived rules to enhance performance, with implementation results compared to UPPAAL.

Contribution

First algorithm for model checking a rich mu-calculus over timed automata using proof search and derived rules for improved efficiency.

Findings

Algorithm is sound and complete.

Performance improvements with derived rules.

Comparison shows competitive results with UPPAAL.

Abstract

This paper presents the first model-checking algorithm for an expressive modal mu-calculus over timed automata, $L^{\mathit{rel}, \mathit{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; we encode our algorithm in these proof rules and model-check 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 \emph{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 compare our implementation of this model checker to the UPPAAL tool.