Verification of Concurrent Infinite State Systems 

Axis : SciLex
Subject : reachability, model checking and equivalence checking of concurrent infinite state systems
Coordinator : Stefan Göller
  • P1: Laboratoire Spécification et Vérification in Cachan (France) - Alain Finkel, Stéphane Demri, Sylvain Schmitz, Philippe Schnoebelen, Stefan Schwoon)
  • P2: Laboratoire d‘Informatique Algorithmique: Fondaments et Applications in Paris (France - (Peter Habermehl, Olivier Serre)
  • P3: Laboratoire d‘Informatique de l‘Institut Gaspard Monge in Marne-La-Vallée (France (Arnaud Carayol)
  • P4: Laboratoire Bordelais de Recherche en Informatique in Bordeaux (France)-(Jérôme Leroux, Géraud Sénizergues, Grégoire Sutre)
  • P5: Max-Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern (Germany)- Dmitry Chistikov, Rupak Majumdar)
  • P6: Department of Computer Science at Technical University of Ostrava (Czech Republic)- Stanislav Böhm, Petr Jancar)
Candidat: Georg Zetzsche (Post-doc), Christoph Haase (Post-doc), Piotr Hofman (Post-doc)
Host Laboratory : LSV Cachan
DigiCosme funding : 2014/2017

This research project aims to investigate the central issues of research on accessibility, model verification and equivalence verification of models of infinite state systems that model competition. This field of research is young and active on the one hand, but also complex and very poorly understood on the other. Our objective is to better understand the algorithmic behaviour of simultaneous infinite state systems with respect to the formal verification tasks mentioned above.

In a very general way, we would like to answer the following questions. First, when is the respective verification task decidable, i.e. when can it be solved efficiently on a computer? Second, if the respective verification task is decidable, how many resources in terms of time and space are sufficient and necessary to solve it on a computer?



Transversal project: