Verification of Concurrent Infinite State Systems
Axe :SciLex
Sujet : reachability, model checking and equivalence checking of concurrent infinite state systems
Coordinateur : Stefan Göller
Equipe:
- 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)
Candidats: Georg Zetzsche (Post-doc), Christoph Haase (Post-doc), Piotr Hofman (Post-doc)
Laboratoire : LSV Cachan
Durée du projet : 2014/2017
Introduction
Ce projet de recherche vise à étudier les questions centrales de la recherche sur l’accessibilité, la vérification des modèles et la vérification de l’équivalence des modèles de systèmes à états infinis qui permettent de modéliser la concurrence. Ce domaine de recherche est jeune et actif d’une part, mais aussi complexe et très mal compris d’autre part. Notre objectif est de mieux comprendre le comportement algorithmique des systèmes à états infinis simultanés en ce qui concerne les tâches de vérification formelle mentionnées ci-dessus.
D’une manière très générale, nous aimerions répondre aux questions suivantes. Premièrement, quand la tâche de vérification respective est-elle décidable, c’est-à-dire quand peut-elle être résolue efficacement sur ordinateur ? Deuxièmement, dans le cas où la tâche de vérification respective est décidable, combien de ressources en termes de temps et d’espace sont suffisantes et nécessaires pour la résoudre sur ordinateur ?
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)
Projet transverse :