Model-checking, Timed automata, Abstract zone graph, Dynamic abstraction, State-space exploration strategy, Partial-order techniques

Timed automata (AD94) is a widely accepted model for real-time system verification. Formal verification algorithms usually perform a state-space exploration of the automaton to ensure that a given specification is satisfied. The state-space of a timed automaton is uncountable. Hence, algorithms rely on finite abstractions that faithfully represent the state-space of the automaton. Alur and Dill introduced the region graph abstraction in (AD94), however this approach does not scale beyond very simple timed automata. Several abstractions have been introduced based on zone graphs that allowed scale formal verification to timed automata modeling industrial case studies (DT98, BBFL03, BBLP06, HSW16, GHSW19). In parallel, several optimisations of the state-space exploration algorithms have been proposed (DT98, HSW13, HT15, RSM19).

The goal of this internship is to combine several of the optimisations above in a new algorithm that improves state-of-the-art approaches. We particularly focus on the following techniques:

- dynamic abstractions (HSW13,RSM19) that start from a coarse abstraction and refine it during state-space exploration, in order to preserve reachability properties while keeping the abstraction as coarse as possible;
- partial-order semantics (GHSW19) that introduces an alternative, yet equivalent, definition of time that better takes into account the concurrency in timed automata that consist in many concurrent processes;
- topological search (HT15) that guides the state-space exploration in order to avoid visiting and storing useless states, leading to a huge reduction in computation time and memory usage.

Combining these three techniques is far from obvious as, for instance, some of them rely on incompatible exploration strategies of the state-space. The goal of this internship is to study the core ideas behind these techniques and to propose a new algorithm that benefit from them. The new algorithm will be implemented in the tool TChecker (TCK) and evaluated on standard benchmarks from the litterature.

- (AD94) Alur R. and Dill D.: A theory of timed automata. Theoretical Computer Science 1994.
- (DT98) Daws C. and Tripakis S.: Model Checking of Real-Time Reachability Properties Using Abstractions. TACAS 1998.
- (BBFL03) Behrmann G., Bouyer P., Fleury E., Larsen K.G.: Static Guard Analysis in Timed Automata Verification. TACAS 2003.
- (BBLP06) Behrmann G., Bouyer P., Larsen K. G. and Pelánek R.: Lower and upper bounds in zone-based abstractions of timed automata. Int. J. Softw. Tools Technol. Transf. 2006.
- (HSW16) Herbreteau F., B. Srivathsan, Walukiewicz I.: Better abstractions for timed automata. Inf. Comput. 2016.
- (HT15) Herbreteau F., Tran, T.-T.: Improving Search Order for Reachability Testing in Timed Automata. FORMATS 2015.
- (HSW13) Herbreteau F., B. Srivathsan, Walukiewicz I.: Lazy Abstractions for Timed Automata. CAV 2013.
- (RSM19) Roussanaly V., Sankur O. and Markey N.: Abstraction Refinement Algorithms for Timed Automata. CAV 2019.
- (GHSW19) Govind R., Herbreteau F., B. Srivathsan, Walukiewicz I.: Revisiting Local Time Semantics for Networks of Timed Automata. CONCUR 2019.
- (TCK) https://github.com/ticktac-project/tchecker