The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Abstract regular tree model checking (ARTMC) is a generic technique for automated formal verification of various kinds of
infinite-state and parameterised systems, including, e.g., parameterised protocols or programs manipulating dynamic,
pointer-linked data structures. ARTMC is based on representing infinite sets of configurations of the examined systems by finite
tree automata whose efficient manipulation is thus crucial for an overall efficiency of ARTMC. It turns out that a significant
bottleneck in dealing with finite tree automata is the need to determinise them when checking inclusion or within the classical
automata minimisation procedure. In the talk, we will present several recent works whose aim is to eliminate the need to
determinise the automata being handled in ARTMC.
In particular, we will present methods for an antichain-based inclusion checking on nondeterministic tree automata and efficient
methods for reducing the size of such automata based on various types of upward, downward, and composed (bi)simulations.
According to our experimental results, these techniques really very significantly improve the performance of ARTMC.
The talk is based on joint work with Ahmed Bouajjani and Tayssir Touili from LIAFA, Peter Habermehl from LSV,
Parosh Aziz Abdulla and Lisa Kaati from Uppsala, and Lukas Holik from FIT BUT.