LSV Seminar

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.

Past Seminars

Regular Model Checking using nondeterministic tree automata

Tuesday, July 08 2008 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Tomas Vojnar (FIT Technical University Brno)

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.

About LSV