Alladi Ramakrishnan Hall

Towards Efficient Verification of Timed Systems: Theory and Practice

Govind R

Uppsala University,

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 untimed setting, the approach to the model-checking problem involves reducing it to the reachability problem on the product of the network of automata that models the system and the automaton corresponding to the negation of the logical formula. Thus, an efficient procedure for the model-checking problem hinges on two fundamental challenges: (1) an efficient logic-to-automata translation, and (2) efficient techniques to address state-space explosion due to interleavings in the networks that model the system.


The focus of this talk is on the timed setting of the model checking problem. Here, 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. Even though these formalisms have been the subject of extensive research since their introduction in the early 90s, the success of classical model-checking has not translated to real-time systems. In this talk, I will discuss some of my work that aims to address two fundamental bottlenecks in model-checking real-time systems.


Efficient reachability procedure for networks of timed automata: We come up with solutions for alleviating the effects of state-space explosion, based on the ideas of partial order reduction and an alternate semantics for timed networks, called local-time semantics (Bengtsson et al; CONCUR ‘98). We design the first procedure that uses local-time semantics to check reachability, which is the current state-of-the-art for timed networks.


Efficient logic-to-automata translation: We propose a new model, called Generalized Timed Automata (GTA) by extending timed automata and provide a logic-to-automata translation from MITL to GTA. Our model has several powerful features that allows one to model various behaviours of real-time systems more succinctly, which results in automata with fewer states, transitions and clocks.


Based on the following works


Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods. R. Govind, Frèdèric Herbreteau, B. Srivathsan and Igor Walukiewicz. Symposium on Logic in Computer Science (LICS) 2022.

A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation. S. Akshay, Paul Gastin, R. Govind, Aniruddha R. Joshi and B. Srivathsan. International Conference on Computer Aided Verification (CAV) 2023.

Here is the link:

Please find the link as requested

Join Zoom Meeting
zoom.us/j/99598370034

Meeting ID: 995 9837 0034
Passcode: 941422