Publications

2022

1. Accepted at TOCL

   Continuous One-Counter Automata Blondin, Michael, Leys, Tim, Mazowiecki, Filip, Offtermatt, Philip, and Pérez, Guillermo A. 2022 [Abs]

   We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is NP-complete for COCA with parametric counter updates and bound tests.

2. Accepted at CAV

   Verifying generalised and structural soundness of workflow nets via relaxations Blondin, Michael, Mazowiecki, Filip, and Offtermatt, Philip 2022 [HTML]
3. Accepted at LICS

   The complexity of soundness in workflow nets Blondin, Michael, Mazowiecki, Filip, and Offtermatt, Philip 2022 [HTML]

2021

1. LICS

   Continuous One-Counter Automata Blondin, Michael, Leys, Tim, Mazowiecki, Filip, Offtermatt, Philip, and Pérez, Guillermo A. In 36th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 2021 2021 [Abs] [HTML]

   We study the reachability problem for continuous one-counter automata, COCA for short. In such automata, transitions are guarded by upper and lower bound tests against the counter value. Additionally, the counter updates associated with taking transitions can be (non-deterministically) scaled down by a nonzero factor between zero and one. Our three main results are as follows: (1) We prove that the reachability problem for COCA with global upper and lower bound tests is in NC2; (2) that, in general, the problem is decidable in polynomial time; and (3) that it is decidable in the polynomial hierarchy for COCA with parametric counter updates and bound tests.

2. TACAS

   Directed Reachability for Infinite-State Systems Blondin, Michael, Haase, Christoph, and Offtermatt, Philip In International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2021 [Abs] [HTML]

   Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as A* and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.

2019

1. TACAS

   Computing the expected execution time of probabilistic workflow nets Meyer, Philipp J, Esparza, Javier, and Offtermatt, Philip In International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2019 [HTML]
2. Thesis

   Approaching Safety for Parameterized Systems via View Abstraction Offtermatt, Philip 2019 [PDF]

2017

1. Thesis

   A Tool for Verification and Simulation of Population Protocols Offtermatt, Philip 2017 [PDF]