Model Checking for Real-time Systems using Generalized Timed Automata

Model checking for real-time systems is a fundamental problem in formal verification. The goal here is to check whether a system (modelled as a network of automata) satisfies a specification (provided by a logical formula). In the timed setting, Timed Automata serve as a well-established model for real-time systems, with Metric Interval Temporal Logic (MITL) being the standard formalism for specifying properties. One of the central challenges here is an efficient logic-to-automata translation for Metric Interval Temporal Logic (MITL). Recently, we proposed a new model, called Generalized Timed Automata (GTA), that unifies the features of various models such as timed automata, event-clock automata, and automata with timers. The model comes with several powerful additional features, and yet, the best known zone-based reachability algorithms for timed automata have been extended to the GTA model, with the same complexity for all the zone operations. In this work, we first propose a logic-to-automata translation from MITL to GTA. Our modular translation leverages the powerful features of GTA to generate automata with fewer states, transitions, and clocks. Further, since the various formalisms used for modelling real-time systems are also captured by GTAs, thanks to this translation, MITL model checking reduces to checking liveness for GTAs. However, no liveness algorithm is known for GTAs. The liveness algorithms for timed automata crucially rely on the presence of a finite time-abstract bisimulation, while such a relation is known not to exist for GTAs. As our second contribution, we propose the first algorithm for checking Büchi non-emptiness in GTAs, which circumvents this fundamental challenge. Joint work with S Akshay, Paul Gastin and B Srivathsan.

Authors

• R Govind

Keywords

No keywords are indexed for this paper.