Translations
VERICONISS
Verification of Concurrent Infinite State Systems
Axis : SciLex
Subject : reachability, model checking and equivalence checking of concurrent infinite state systems
Coordinator : Stefan Göller
Team::
- 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)
Host Laboratory : LSV Cachan
DigiCosme funding : 2014/2017
Introduction
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?
Documents:
Publications
- Decidability, Complexity, and Expressiveness of First-Order Logic Over the Subword Ordering In LICS'17 (S. Halfon and P. Schnoebelen and G. Zetzsche)
- On long words avoiding Zimin patterns In STACS'17 (A. Carayol and S. Göller)
- On Büchi one-counter automata In STACS'17 (S. Böhm, S. Göller, S. Halfon and P. Hofman)
- On the Parallel Complexity of Bisimulation over Finite Systems In CSL'16 (M. Ganardi, S. Göller and M. Lohrey)
- Games with bound guess actions In LICS'16 (Th. Colcombet and S. Göller)
- The Taming of the Semi-Linear Set In ICALP'16 (D. Chistikov and C. Haase)
- A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One In ICALP'16 (S. Göller, C. Haase, R. Lazić and P. Totzke)
- Approaching the Coverability Problem Continuously In TACAS'16 (M. Blondin, A. Finkel, C. Haase and S. Haddad)
- The Complexity of the Kth Largest Subset Problem and Related Problems In Information Processing Letters 116(2) (C. Haase and S. Kiefer)
- Complexity of regular abstractions of one-counter languages In LICS'16 (M. F. Atig, D. Chistikov, P. Hofman, K. N. Kumar, P. Saivasan and G. Zetzsche)
- Shortest paths in one-counter systems In FoSSaCS'16 (D. Chistikov, W. Czerwiński, P. Hofman, M. Pilipczuk and M. Wehar)
- Tightening the Complexity of Equivalence Problems for Commutative Grammars In STACS'16 (C. Haase and P. Hofman)
- Coverability Trees for Petri Nets with Unordered Data In FoSSaCS'16 (P. Hofman, S. Lasota, R. Lazić, J. Leroux, S. Schmitz and P. Totzke)
- Active Diagnosis with Observable Quiescence. In CDC'15 (S. Böhm, S. Haar, S. Haddad, P. Hofman and S. Schwoon)
- The Odds of Staying on Budget In ICALP'15 (C. Haase and S. Kiefer)
- Reachability in Two-Dimensional Vector Addition Systems with States is PSPACE-Complete In LICS'15 (M. Blondin, A. Finkel, S. Göller, C. Haase and P. McKenzie)
Transversal project: