# VERICONISS

# Verification of Concurrent Infinite State Systems

**Action line:**SciLex

**Subject :**reachability, model checking and equivalence checking of concurrent infinite state systems

**Project Coordinator :**Stefan Göller

**Current Member :**Georg Zetzsche (Post-doc)

**Former Members :**Christoph Haase (Post-doc), Piotr Hofman (Post-doc)

**Host Laboratory :**LSV Cachan

**DigiCosme Funding :**2014/2017

**Introduction**

This research project plans to investigate the central research questions of reachability, model checking and equivalence checking of models of infinite state systems that allow to model concurrency . This area of research is young and active on the one hand, but also complex and very badly understood on the other. We aim at developing a better understanding of how concurrent infinite state systems behave algorithmically with respect to the above-mentioned formal verification tasks.

Very generally speaking we would like to provide answers to the following questions. Firstly, when is the respective verification task decidable, i.e. when can it effectively be solved on computers? Secondly, in case the respective verification task is decidable, how many resources in terms of time and space consumption are sufficient and necessary to solve it on computers?

**Documents**:

**Scientific productions :**

- 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)

**Interdisciplinary work :**