Patrick Totzke | publications

The Power of Counting Steps in Quantitative Games

Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke and Pierre Vandenhove

Abs Bib pdf

We study games of infinite duration played on graphs and focus on the strategy complexity of quantitative objectives. Such games are known to admit optimal memoryless strategies over finite graphs, but require infinite-memory strategies in general over infinite graphs.

We provide new lower and upper bounds for the strategy complexity of mean-payoff and total-payoff objectives over infinite graphs, focusing on whether step-counter strategies (sometimes called Markov strategies) suffice to implement winning strategies. In particular, we show that over finitely branching arenas, three variants of \(\limsup\) mean-payoff and total-payoff objectives admit winning strategies that are based either on a step counter or on a step counter and an additional bit of memory. Conversely, we show that for certain \(\liminf\) total-payoff objectives, strategies resorting to a step counter and finite memory are not sufficient. For step-counter strategies, this settles the case of all classical quantitative objectives up to the second level of the Borel hierarchy.
```
@misc{BIPTV2024,
  title = {{The Power of Counting Steps in Quantitative Games}},
  author = {Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},
  year = {2024}
}
```
Strategy Complexity of Büchi Objectives in Concurrent Stochastic Games

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

Abs Bib arXiv

We study 2-player concurrent stochastic Büchi games on countable graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of visiting a set of target states infinitely often. We show that there always exist \(\varepsilon\)-optimal Max strategies that use just a step counter plus 1 bit of public memory. This upper bound holds for all countable graphs, but it is a new result even for the special case of finite graphs. The upper bound is tight in the sense that Max strategies that use just a step counter, or just finite memory, are not sufficient even on finite game graphs.

The upper bound is a consequence of a slightly stronger new result: \eps-optimal Max strategies for the combined Büchi and Transience objective require just 1 bit of public memory (but cannot be memoryless). Our proof techniques also yield a closely related result, that \eps-optimal Max strategies for the Transience objective alone (which is only meaningful in infinite graphs) can be memoryless.
```
@misc{KMST2024a,
  title = {Strategy Complexity of B\"uchi Objectives in Concurrent
  		  Stochastic Games},
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  year = {2024}
}
```
Memoryless Strategies in Stochastic Reachability Games

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

(To appear in Lecture Notes in Computer Science)

Abs Bib arXiv

We study concurrent stochastic reachability games played on finite graphs. Two players, Max and Min, seek respectively to maximize and minimize the probability of reaching a set of target states. We prove that Max has a memoryless strategy that is optimal from all states that have an optimal strategy. Our construction provides an alternative proof of this result by Bordais, Bouyer and Le Roux, and strengthens it, as we allow Max’s action sets to be countably infinite.
```
@misc{KMST2024,
  title = {Memoryless Strategies in Stochastic Reachability Games},
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  year = {2024},
  note = {To appear in Lecture Notes in Computer Science}
}
```
Strategy Complexity of Reachability in Countable Stochastic 2-Player Games

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

(To appear in Dynamic Games and Applications)

Abs Bib arXiv

We study countably infinite stochastic 2-player games with reachability objectives. Our results provide a complete picture of the memory requirements of \(\varepsilon\)-optimal (resp. optimal) strategies. These results depend on whether the game graph is infinitely branching and on whether one requires strategies that are uniform (i.e., independent of the start state). Our main result is that \(\varepsilon\)-optimal (resp. optimal) Maximizer strategies in infinitely branching turn-based reachability games require infinite memory. This holds even under very strong restrictions. Even if all states have an almost surely winning Maximizer strategy, strategies with a step counter plus finite private memory are still useless. Regarding uniformity, we show that for Maximizer there need not exist positional uniformly \(\varepsilon\)-optimal strategies even in finitely branching turn-based games, whereas there always exists one that uses one bit of public memory, even in concurrent games with finite action sets.
```
@misc{KMST2022,
  title = {Strategy Complexity of Reachability in Countable
  		  Stochastic 2-Player Games},
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  year = {2022},
  note = {To appear in Dynamic Games and Applications}
}
```
Bounded-Memory Strategies in Partial-Information Games

Sougata Bose, Rasmus Ibsen-Jensen, and Patrick Totzke

Abs Bib

We study the computational complexity of solving stochastic games with mean-payoff objectives. Instead of identifying special classes in which simple strategies are sufficient to play \(\varepsilon\)-optimally, or form \(\varepsilon\)-Nash equilibria, we consider general partial-information, multiplayer games and ask what can be achieved with (and against) finite-memory strategies up to a given bound on the memory.

We show NP-hardness for approximating zero-sum values, already with respect to memoryless strategies and for 1-player reachability games. On the other hand, we provide upper bounds for solving games of any fixed number of players k. We show that one can decide in polynomial space if, for a given k-player game, \(\varepsilon\ge 0 \) and bound b, there exists an \(\varepsilon\)-Nash equilibrium in which all strategies use at most b memory modes. For given \(\varepsilon > 0\), finding an \(\varepsilon\)-Nash equilibrium with respect to b-bounded strategies can be done in \(\text{FNP}^{\text{NP}}\). Similarly, for zero-sum games finding a b-bounded strategy that, against all b-bounded opponent strategies, guarantees an outcome within \(\varepsilon\)of a given value, can be done in \(\text{FNP}^{\text{NP}}\). Our constructions apply to parity objectiveswith minimal simplifications.

Our results improve the status quo in several well-known special cases of games. In particular, for 2-player zero-sum concurrent mean-payoff games, our results imply that one can approximate ordinary zero-sum values (without restricting admissible strategies) in \(\text{FNP}^{\text{NP}}\).
```
@misc{BIT2024,
  title = {Bounded-Memory Strategies in Partial-Information Games},
  author = {Bose, Sougata and Ibsen{-}Jensen, Rasmus and Totzke, Patrick},
  year = {2024}
}
```
History-deterministic Timed Automata

Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke

(To appear in Logical Methods in Computer Science )

Abs Bib arXiv pdf

We explore the notion of history-determinism in the context of timed automata (TA) over infinite timed words. History-deterministic (HD) automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and HD specifications allow for game-based verification without an expensive determinization step.

We show that the class of timed \(ω\)-languages recognised by HD timed automata strictly extends that of deterministic ones, and is strictly included in those recognised by fully non-deterministic TA.

For non-deterministic timed automata it is known that universality is already undecidable for Büchi TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are -complete.

For the subclass of TA with safety or reachability acceptance, one can decide (in EXPTIME) whether such an automaton is history-deterministic. If so, it can effectively determinized without introducing new automata states.
```
@misc{BHLST2023,
  title = {History-deterministic Timed Automata},
  author = {Bose, Sougata and Henzinger, Thomas A. and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},
  year = {2023},
  note = {To appear in Logical Methods in Computer Science }
}
```
Controlling a Random Population is EXPTIME-hard

Corto Mascle, Mahsa Shirmohammadi, and Patrick Totzke

Abs Bib arXiv pdf

Bertrand et al. (LMCS 2019) describe two-player zero-sum games in which one player tries to achieve a reachability objective in n games (on the same finite arena) simultaneously by broadcasting actions, and where the opponent has full control of resolving non-deterministic choices. They show EXPTIME completeness for the question if such games can be won for every number n of games.

We consider the almost-sure variant in which the opponent randomizes their actions, and where the player tries to achieve the reachability objective eventually with probability one. The lower bound construction in [1] does not directly carry over to this randomized setting. In this note we show EXPTIME hardness for the almost-sure problem by reduction from Countdown Games.
```
@misc{MST2019,
  title = {Controlling a Random Population is EXPTIME-hard},
  author = {Mascle, Corto and Shirmohammadi, Mahsa and Totzke, Patrick},
  year = {2019}
}
```

Parity Games on Temporal Graphs

Pete Austin, Sougata Bose, and Patrick Totzke

In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2024

Abs Bib arXiv doi pdf

Temporal graphs are a popular modelling mechanism for dynamic complex systems that extend ordinary graphs with discrete time. Simply put, time progresses one unit per step and the availability of edges can change with time.

We consider the complexity of solving \(ω\)-regular games played on temporal graphs where the edge availability is ultimately periodic and fixed a priori.

We show that solving parity games on temporal graphs is decidable in PSPACE, only assuming the edge predicate itself is in PSPACE. A matching lower bound already holds for what we call punctual reachability games on static graphs, where one player wants to reach the target at a given, binary encoded, point in time. We further study syntactic restrictions that imply more efficient procedures. In particular, if the edge predicate is in \(P\ \)and is monotonically increasing for one player and decreasing for the other, then the complexity of solving games is only polynomially increased compared to static graphs.
```
@inproceedings{ABT2024,
  title = {Parity Games on Temporal Graphs},
  author = {Austin, Pete and Bose, Sougata and Totzke, Patrick},
  editor = {Kobayashi, Naoki and Worrell, James},
  booktitle = {International Conference on Foundations of Software
  		  Science and Computational Structures (FoSSaCS)},
  series = {Lecture Notes in Computer Science},
  volume = {14574},
  pages = {79--98},
  publisher = {Springer},
  year = {2024},
  url = {https://doi.org/10.1007/978-3-031-57228-9\_5},
  doi = {10.1007/978-3-031-57228-9\_5}
}
```

2023

History-Deterministic Vector Addition Systems

Sougata Bose, David Purser, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2023

Abs Bib arXiv doi pdf

We consider history-determinism, a restricted form of non-determinism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words, both with coverability and reachability acceptance. History-determinism requires that the non-deterministic choices can be resolved on-the-fly; based on the past and without jeopardising acceptance of any possible continuation of the input word.

Our results show that the history-deterministic (HD) VASS sit strictly between deterministic and non-deterministic VASS regardless of the number of counters. We compare the relative expressiveness of HD systems, and closure-properties of the induced language classes, with coverability and reachability semantics, with and without silent (\(\varepsilon\)-labelled) transitions.

Whereas in dimension 1, inclusion and regularity remain decidable, from dimension two onwards, HD-VASS with suitable resolver strategies, are essentially able to simulate 2-counter Minsky machines, leading to several undecidability results: It is undecidable whether an VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable.
```
@inproceedings{BPT2023,
  title = {{History-Deterministic Vector Addition Systems}},
  author = {Bose, Sougata and Purser, David and Totzke, Patrick},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  year = {2023},
  pages = {18:1--18:17},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-299-0},
  issn = {1868-8969},
  volume = {279},
  editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2023/19012},
  urn = {urn:nbn:de:0030-drops-190120},
  doi = {10.4230/LIPIcs.CONCUR.2023.18}
}
```

Handling of Past and Future with Phenesthe+

Manolis Pitsikalis, Alexei Lisitsa, Patrick Totzke and Simon Lee

In International Symposium on Games, Automata, Logics, and Formal Verification (GandALF), 2023

Bib arXiv

@inproceedings{PLT2023,
  author = {Pitsikalis, Manolis and Lisitsa, Alexei and Totzke, Patrick and Lee, Simon},
  booktitle = {International Symposium on Games, Automata, Logics, and
  		  Formal Verification (GandALF)},
  title = {Handling of Past and Future with Phenesthe+},
  year = {2023}
}

2022

History-deterministic Timed Automata are Not Determinizable

Sougata Bose, Thomas A. Henzinger, Karoliina Lehtinen, Sven Schewe, and Patrick Totzke

In International Workshop on Reachability Problems (RP), 2022

Abs Bib pdf

An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata, where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones.

We provide a proof for this fact.
```
@inproceedings{BHLST2022,
  title = {History-deterministic Timed Automata are Not
  		  Determinizable},
  author = {Bose, Sougata and Henzinger, Thomas A. and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},
  year = {2022},
  booktitle = {International Workshop on Reachability Problems (RP)}
}
```
History-deterministic Timed Automata

Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2022

Abs Bib pdf slides

We explore the notion of history-determinism in the context of timed automata (TA). History-deterministic automata are those in which nondeterminism can be resolved on the fly, based on the run constructed thus far. History-determinism is a robust property that admits different game-based characterisations, and history-deterministic specifications allow for game-based verification without an expensive determinization step.

We show yet another characterisation of history-determinism in terms of fair simulation, at the general level of labelled transition systems: a system is history-deterministic precisely if and only if it fairly simulates all language smaller systems.

For timed automata over infinite timed words it is known that universality is undecidable for Büchi TA. We show that for history-deterministic TA with arbitrary parity acceptance, timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-complete.

For the subclass of TA with safety or reachability acceptance, we show that checking whether such an automaton is history-deterministic is decidable (in EXPTIME), and history-deterministic TA with safety acceptance are effectively determinizable without introducing new states.
```
@inproceedings{HLT2022,
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  title = {History-deterministic Timed Automata},
  author = {Henzinger, Thomas A. and Lehtinen, Karoliina and Totzke, Patrick},
  year = {2022}
}
```

Making Sense of Heterogeneous Maritime Data

Manolis Pitsikalis, Alexei Lisitsa, Patrick Totzke and Simon Lee

In International Conference on Mobile Data Management (MDM), 2022

Bib doi

@inproceedings{PLT2022,
  author = {Pitsikalis, Manolis and Lisitsa, Alexei and Totzke, Patrick and Lee, Simon},
  booktitle = {International Conference on Mobile Data Management (MDM)},
  title = {Making Sense of Heterogeneous Maritime Data},
  year = {2022},
  volume = {},
  number = {},
  pages = {401-406},
  doi = {10.1109/MDM55031.2022.00089}
}

2021

Transience in Countable MDPs

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2021

Abs Bib arXiv doi pdf teaser
The Transient objective is not to visit any state infinitely often. While this is not possible in any finite Markov Decision Process (MDP), it can be satisfied in countably infinite ones, e.g., if the transition graph is acyclic.

We prove the following fundamental properties of Transient in countably infinite MDPs.
1. There exist uniformly \(\varepsilon\)-optimal MD strategies (memoryless deterministic) for Transient, even in infinitely branching MDPs.
2. Optimal strategies for Transient need not exist, even if the MDP is finitely branching. However, if an optimal strategy exists then there is also an optimal MD strategy.
3. If an MDP is universally transient (i.e., almost surely transient under all strategies) then many other objectives have a lower strategy complexity than in general MDPs. E.g., \(\varepsilon\)-optimal strategies for Safety and co-Büchi and optimal strategies for \(\{0,1,2\}\)-Parity (where they exist) can be chosen MD, even if the MDP is infinitely branching.
```
@inproceedings{KMST2021,
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title = {{Transience in Countable MDPs}},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  pages = {11:1--11:15},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-203-7},
  issn = {1868-8969},
  year = {2021},
  volume = {203},
  editor = {Haddad, Serge and Varacca, Daniele},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14388},
  urn = {urn:nbn:de:0030-drops-143881},
  doi = {10.4230/LIPIcs.CONCUR.2021.11}
}
```
HyperLTL Satisfiability is \(\Sigma_1^1\)-complete, HyperCTL* Satisfiability is \(\Sigma_1^2\)-complete

Marie Fortin, Louwe B. Kuijer, Patrick Totzke and Martin Zimmermann

In International Symposium on Mathematical Foundations of Computer Science (MFCS), 2021

Abs Bib arXiv doi

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i.e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is \(\Sigma_1^1\)-complete and HyperCTL* satisfiability is \(\Sigma_1^2\)-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove \(\Sigma_1^2\)-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is \(\Pi_1^1\)-complete.
```
@inproceedings{FKTZ2021,
  author = {Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},
  title = {{HyperLTL Satisfiability is \(\Sigma_1^1\)-complete,
  		  HyperCTL* Satisfiability is \(\Sigma_1^2\)-complete}},
  booktitle = {International Symposium on Mathematical Foundations of
  		  Computer Science (MFCS)},
  pages = {47:1--47:19},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-201-3},
  issn = {1868-8969},
  year = {2021},
  volume = {202},
  editor = {Bonchi, Filippo and Puglisi, Simon J.},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2021/14487},
  urn = {urn:nbn:de:0030-drops-144870},
  doi = {10.4230/LIPIcs.MFCS.2021.47}
}
```
Simple Stochastic Games with Almost Sure Energy-Parity Objectives

Richard Mayr, Sven Schewe, Patrick Totzke and Dominik Wojtczak

In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2021

Abs Bib arXiv pdf

We study stochastic games with energy-parity objectives, which combine quantitative rewards with a qualitative ω-regular condition: The maximizer aims to avoid running out of energy while simultaneously satisfying a parity condition. We show that the corresponding almost-sure problem, i.e., checking whether there exists a maximizer strategy that achieves the energy-parity objective with probability 1 when starting at a given energy level k, is decidable and in NP∩coNP. The same holds for checking if such a k exists and if a given k is minimal.
```
@inproceedings{MSTW2021,
  author = {Mayr, Richard and Schewe, Sven and Totzke, Patrick and Wojtczak, Dominik},
  title = {{Simple Stochastic Games with Almost Sure Energy-Parity
  		  Objectives}},
  booktitle = {International Conference on Foundations of Software
  		  Science and Computational Structures (FoSSaCS)},
  year = {2021}
}
```

2020

Optimally Resilient Strategies in Pushdown Safety Games

Daniel Neider, Patrick Totzke and Martin Zimmermann

In International Symposium on Mathematical Foundations of Computer Science (MFCS), 2020

Bib arXiv doi pdf

@inproceedings{NTZ2020,
  author = {Neider, Daniel and Totzke, Patrick and Zimmermann, Martin},
  title = {{Optimally Resilient Strategies in Pushdown Safety
  		  Games}},
  booktitle = {International Symposium on Mathematical Foundations of
  		  Computer Science (MFCS)},
  pages = {74:1--74:15},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-159-7},
  issn = {1868-8969},
  year = {2020},
  volume = {170},
  editor = {Esparza, Javier and Kr{\'a}ľ, Daniel},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/12743},
  doi = {10.4230/LIPIcs.MFCS.2020.74}
}

How to Play in Infinite MDPs (Invited)

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke and Dominik Wojtczak

In International Colloquium on Automata, Languages and Programming (ICALP), 2020

Bib doi pdf

@inproceedings{KMST2020,
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick and Wojtczak, Dominik},
  title = {{How to Play in Infinite MDPs (Invited)}},
  booktitle = {International Colloquium on Automata, Languages and
  		  Programming (ICALP)},
  pages = {3:1--3:18},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-138-2},
  issn = {1868-8969},
  year = {2020},
  volume = {168},
  editor = {Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/12410},
  doi = {10.4230/LIPIcs.ICALP.2020.3}
}

Strategy Complexity of Parity Objectives in Countable MDPs

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2020

Bib arXiv doi pdf

@inproceedings{KMST2020a,
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title = {{Strategy Complexity of Parity Objectives in Countable
  		  MDPs}},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  pages = {39:1--39:17},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-160-3},
  issn = {1868-8969},
  year = {2020},
  volume = {171},
  editor = {Konnov, Igor and Kov{\'a}cs, Laura},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/12851},
  doi = {10.4230/LIPIcs.CONCUR.2020.39}
}

Parametrized Universality Problems for One-Counter Nets

Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2020

Bib doi pdf Video teaser

@inproceedings{ABHT2020,
  author = {Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},
  title = {{Parametrized Universality Problems for One-Counter
  		  Nets}},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  pages = {47:1--47:16},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-160-3},
  issn = {1868-8969},
  year = {2020},
  volume = {171},
  editor = {Konnov, Igor and Kov{\'a}cs, Laura},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/12859},
  doi = {10.4230/LIPIcs.CONCUR.2020.47},
  video = { https://www.youtube.com/watch?v=eJjMcgKK4bg}
}

2019

Timed Basic Parallel Processes

Lorenzo Clemente, Piotr Hofman, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2019

Bib doi pdf

@inproceedings{CHT2019,
  author = {Clemente, Lorenzo and Hofman, Piotr and Totzke, Patrick},
  title = {Timed Basic Parallel Processes},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  pages = {15:1--15:16},
  year = {2019},
  url = {https://doi.org/10.4230/LIPIcs.CONCUR.2019.15},
  doi = {10.4230/LIPIcs.CONCUR.2019.15}
}

Büchi Objectives in Countable MDPs

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke

In International Colloquium on Automata, Languages and Programming (ICALP), 2019

Bib doi pdf

@inproceedings{KMST2019,
  author = {Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title = {B{\"{u}}chi Objectives in Countable MDPs},
  booktitle = {International Colloquium on Automata, Languages and
  		  Programming (ICALP)},
  year = {2019},
  pages = {119:1--119:14},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH,
  		  Wadern/Saarbruecken, Germany},
  copyright = {Creative Commons Attribution 3.0 Unported license (CC-BY
  		  3.0)},
  doi = {10.4230/LIPIcs.ICALP.2019.119},
  language = {en},
  url = {https://drops.dagstuhl.de/opus/volltexte/2019/10695/pdf/LIPIcs-ICALP-2019-119.pdf}
}

2018

Universal Safety for Timed Petri Nets is PSPACE-complete

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke

In International Conference on Concurrency Theory (CONCUR), 2018

Bib doi pdf

@inproceedings{AACMT2018,
  author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Ciobanu, Radu and Mayr, Richard and Totzke, Patrick},
  title = {{Universal Safety for Timed Petri Nets is
  		  PSPACE-complete}},
  booktitle = {International Conference on Concurrency Theory (CONCUR)},
  pages = {6:1--6:15},
  series = {Leibniz International Proceedings in Informatics
  		  (LIPIcs)},
  isbn = {978-3-95977-087-3},
  issn = {1868-8969},
  year = {2018},
  volume = {118},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/9544},
  doi = {10.4230/LIPIcs.CONCUR.2018.6}
}

2017

MDPs with Energy-Parity Objectives

Richard Mayr, Sven Schewe, Patrick Totzke and Dominik Wojtczak

In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017

Bib doi pdf slides

@inproceedings{MSTW2017,
  author = {Mayr, Richard and Schewe, Sven and Totzke, Patrick and Wojtczak, Dominik},
  title = {{MDPs with Energy-Parity Objectives}},
  booktitle = {ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  doi = {10.1109/LICS.2017.8005131},
  year = {2017}
}

Linear Combinations of Unordered Data Vectors

Piotr Hofman, Jérôme Leroux, and Patrick Totzke

In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2017

Bib pdf

@inproceedings{HLT2017,
  author = {Hofman, Piotr and Leroux, J{\'e}r{\^o}me and Totzke, Patrick},
  title = { Linear Combinations of Unordered Data Vectors },
  booktitle = {ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2017}
}

2016

Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete

Matthias Englert, Ranko Lazić, and Patrick Totzke

In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2016

Bib pdf slides

@inproceedings{ELT2016,
  author = {Englert, Matthias and Lazi{\'c}, Ranko and Totzke, Patrick},
  title = {Reachability in Two-Dimensional Unary Vector Addition
  		  Systems with States is NL-Complete},
  booktitle = {ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2016}
}

Coverability Trees for Petri Nets with Unordered Data

Piotr Hofman, Slawomir Lasota, Ranko Lazić, Jérôme Leroux, Sylvain Schmitz, and Patrick Totzke

In International Conference on Foundations of Software Science and Computational Structures (FoSSaCS), 2016

Bib pdf

@inproceedings{HLLLST2016,
  title = {{Coverability Trees for Petri Nets with Unordered Data}},
  author = {Hofman, Piotr and Lasota, Slawomir and Lazi{\'c}, Ranko and Leroux, J{\'e}r{\^o}me and Schmitz, Sylvain and Totzke, Patrick},
  url = {https://hal.inria.fr/hal-01252674},
  booktitle = {International Conference on Foundations of Software
  		  Science and Computational Structures (FoSSaCS)},
  year = {2016}
}

A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Stefan Göller, Christoph Haase, Ranko Lazić, and Patrick Totzke

In International Colloquium on Automata, Languages and Programming (ICALP), 2016

Bib pdf

@inproceedings{GHLT2016,
  author = {G{\"{o}}ller, Stefan and Haase, Christoph and Lazi{\'c}, Ranko and Totzke, Patrick},
  title = {A Polynomial-Time Algorithm for Reachability in Branching
  		  {VASS} in Dimension One},
  booktitle = {International Colloquium on Automata, Languages and
  		  Programming (ICALP)},
  year = {2016}
}

2015

On the Coverability Problem for Pushdown Vector Addition Systems in One Dimension

Jérôme Leroux, Grégoire Sutre, and Patrick Totzke

In International Colloquium on Automata, Languages and Programming (ICALP), 2015

Bib arXiv doi pdf slides

@inproceedings{LST2015,
  author = {Leroux, J{\'{e}}r{\^{o}}me and Sutre, Gr{\'{e}}goire and Totzke, Patrick},
  title = {On the Coverability Problem for Pushdown Vector Addition
  		  Systems in One Dimension},
  booktitle = {International Colloquium on Automata, Languages and
  		  Programming (ICALP)},
  year = {2015},
  url = {http://dx.doi.org/10.1007/978-3-662-47666-6_26},
  series = {Lecture Notes in Computer Science},
  volume = {9135},
  pages = {324--336},
  publisher = {Springer},
  doi = {10.1007/978-3-662-47666-6_26}
}

On Boundedness Problems for Pushdown Vector Addition Systems

Jérôme Leroux, Grégoire Sutre, and Patrick Totzke

In International Workshop on Reachability Problems (RP), 2015

Bib arXiv doi pdf slides

@inproceedings{LST2015a,
  author = {Leroux, J{\'{e}}r{\^{o}}me and Sutre, Gr{\'{e}}goire and Totzke, Patrick},
  title = {On Boundedness Problems for Pushdown Vector Addition
  		  Systems},
  year = {2015},
  booktitle = {International Workshop on Reachability Problems (RP)},
  editor = {Bojanczyk, Mikolaj and Lasota, Slawomir and Potapov, Igor},
  series = {Lecture Notes in Computer Science},
  volume = {9328},
  pages = {101--113},
  publisher = {Springer},
  url = {https://doi.org/10.1007/978-3-319-24537-9\_10},
  doi = {10.1007/978-3-319-24537-9\_10}
}

2014

Trace Inclusion for One-Counter Nets Revisited

Piotr Hofman, and Patrick Totzke

In International Workshop on Reachability Problems (RP), 2014

Bib pdf slides

@inproceedings{HT2014,
  author = {Hofman, Piotr and Totzke, Patrick},
  title = {Trace Inclusion for One-Counter Nets Revisited},
  year = {2014},
  booktitle = {International Workshop on Reachability Problems (RP)}
}

Infinite-State Energy Games

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Piotr Hofman, Richard Mayr, K. Narayan Kumar, and Patrick Totzke

In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Bib doi

@inproceedings{AAHMKT2014,
  title = {Infinite-State Energy Games},
  author = {Abdulla, Parosh Aziz and Atig, Mohamed Faouzi and Hofman, Piotr and Mayr, Richard and Kumar, K.~Narayan and Totzke, Patrick},
  booktitle = {ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2014},
  doi = {10.1145/2603088.2603100}
}

2013

Simulation Over One-Counter Nets is PSPACE-Complete

Piotr Hofman, Sławomir Lasota, Richard Mayr, and Patrick Totzke

In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), 2013

Bib pdf

@inproceedings{HLMT2013,
  title = {Simulation Over One-Counter Nets is {PSPACE}-Complete},
  author = {Hofman, Piotr and Lasota, S{\l}awomir and Mayr, Richard and Totzke, Patrick},
  booktitle = {IARCS Annual Conference on Foundations of Software
  		  Technology and Theoretical Computer Science (FSTTCS)},
  year = {2013},
  month = dec
}

Branching-Time Model Checking Gap-Order Constraint Systems

Richard Mayr, and Patrick Totzke

In International Workshop on Reachability Problems (RP), 2013

Bib pdf slides

@inproceedings{MT2013,
  title = {Branching-Time Model Checking Gap-Order Constraint
  		  Systems},
  author = {Mayr, Richard and Totzke, Patrick},
  booktitle = {International Workshop on Reachability Problems (RP)},
  year = {2013},
  month = nov
}

Decidability of Weak Simulation on One-Counter Nets

Piotr Hofman, Richard Mayr, and Patrick Totzke

In ACM/IEEE Symposium on Logic in Computer Science (LICS), 2013

Bib doi pdf slides

@inproceedings{HMT2013,
  title = {Decidability of Weak Simulation on One-Counter Nets},
  author = {Hofman, Piotr and Mayr, Richard and Totzke, Patrick},
  booktitle = {ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2013},
  month = feb,
  doi = {10.1109/LICS.2013.26}
}

2012

Approximating Weak Bisimilarity of Basic Parallel Processes

Piotr Hofman, and Patrick Totzke

In International Workshop on Expressiveness in Concurrency (EXPRESS), 2012

Bib arXiv doi pdf

@inproceedings{HT2012,
  title = {Approximating Weak Bisimilarity of Basic Parallel
  		  Processes},
  author = {Hofman, Piotr and Totzke, Patrick},
  booktitle = {International Workshop on Expressiveness in Concurrency
  		  (EXPRESS)},
  year = {2012},
  month = sep,
  doi = {10.4204/EPTCS.89.8}
}

The Reachability Problem for Two-Dimensional Vector Addition Systems with States

Michael Blondin, Matthias Englert, Alain Finkel, Stefan Göller, Christoph Haase, Ranko Lazić, Pierre Mckenzie, and Patrick Totzke

Journal of the ACM, 2021

Abs Bib doi pdf

We prove that the reachability problem for two-dimensional vector addition systems with states is NL-complete or PSPACE-complete, depending on whether the numbers in the input are encoded in unary or binary. As a key underlying technical result, we show that, if a configuration is reachable, then there exists a witnessing path whose sequence of transitions is contained in a bounded language defined by a regular expression of pseudo-polynomially bounded length. This, in turn, enables us to prove that the lengths of minimal reachability witnesses are pseudo-polynomially bounded.
```
@article{BEFGHLMT2021,
  author = {Blondin, Michael and Englert, Matthias and Finkel, Alain and Göller, Stefan and Haase, Christoph and Lazi\'{c}, Ranko and Mckenzie, Pierre and Totzke, Patrick},
  title = {The Reachability Problem for Two-Dimensional Vector
  		  Addition Systems with States},
  year = {2021},
  issue_date = {October 2021},
  publisher = {Association for Computing Machinery},
  address = {New York, NY, USA},
  volume = {68},
  number = {5},
  issn = {0004-5411},
  url = {https://doi.org/10.1145/3464794},
  doi = {10.1145/3464794},
  journal = {Journal of the {ACM}},
  month = aug,
  articleno = {34},
  numpages = {43}
}
```

What Makes Petri Nets Harder to Verify: Stack or Data?

Ranko Lazić, and Patrick Totzke

Lecture Notes in Computer Science, 2017

Bib doi

@article{LT2017,
  author = {Lazi{\'c}, Ranko and Totzke, Patrick},
  title = {{What Makes Petri Nets Harder to Verify: Stack or Data?}},
  journal = {Lecture Notes in Computer Science},
  volume = {10160},
  number = {1},
  pages = {144--161},
  year = {2017},
  doi = {10.1007/978-3-319-51046-0_8}
}

Branching-Time Model Checking Gap-Order Constraint Systems

Richard Mayr, and Patrick Totzke

Fundamenta Informaticae, 2016

Bib doi

@article{MT2016,
  author = {Mayr, Richard and Totzke, Patrick},
  title = {Branching-Time Model Checking Gap-Order Constraint
  		  Systems},
  journal = {Fundamenta Informaticae},
  volume = {143},
  number = {3-4},
  pages = {339--353},
  year = {2016},
  doi = {10.3233/FI-2016-1317}
}

Simulation Problems Over One-Counter Nets

Piotr Hofman, Slawomir Lasota, Richard Mayr, and Patrick Totzke

Logical Methods in Computer Science , 2016

Bib doi

@article{HLMT2016,
  author = {Hofman, Piotr and Lasota, Slawomir and Mayr, Richard and Totzke, Patrick},
  title = {Simulation Problems Over One-Counter Nets},
  journal = {Logical Methods in Computer Science },
  volume = {12},
  number = {1},
  year = {2016},
  doi = {10.2168/LMCS-12(1:6)2016}
}

Trace inclusion for one-counter nets revisited

Piotr Hofman, and Patrick Totzke

Theoretical Computer Science, 2017

Bib doi

@article{HT2017,
  title = {Trace inclusion for one-counter nets revisited },
  journal = {Theoretical Computer Science},
  volume = {11174},
  year = {2017},
  issn = {0304-3975},
  doi = {10.1016/j.tcs.2017.05.009},
  url = {http://www.sciencedirect.com/science/article/pii/S0304397517303961},
  author = {Hofman, Piotr and Totzke, Patrick}
}

Properties of Multiset Language Classes Defined by Multiset Pushdown Automata

Manfred Kudlek, Patrick Totzke and Georg Zetzsche

Fundamenta Informaticae, 2009

Bib

@article{KTZ09a,
  author = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
  title = {Properties of Multiset Language Classes Defined by
  		  Multiset Pushdown Automata},
  journal = {Fundamenta Informaticae},
  volume = {93},
  number = {(1-3)},
  pages = {235--244},
  year = {2009}
}

Multiset Pushdown Automata

Manfred Kudlek, Patrick Totzke and Georg Zetzsche

Fundamenta Informaticae, 2009

Bib

@article{KTZ2009,
  author = {Kudlek, Manfred and Totzke, Patrick and Zetzsche, Georg},
  title = {Multiset Pushdown Automata},
  journal = {Fundamenta Informaticae},
  year = {2009},
  volume = {93},
  number = {(1-3)},
  pages = {221--233}
}

Inclusion Problems for One-Counter Systems

Patrick Totzke

University of Edinburgh, 2014

Details Bib

@phdthesis{T2014,
  author = {Totzke, Patrick},
  school = {University of Edinburgh},
  title = {{Inclusion Problems for One-Counter Systems}},
  month = apr,
  year = {2014}
}

Multiset Rewriting – A Formal Language Theoretic Perspective on Concurrent Systems

Patrick Totzke

Universität Hamburg, 2009

Bib

@mastersthesis{T2009,
  author = {Totzke, Patrick},
  school = {Universit{\"a}t Hamburg},
  title = {{Multiset Rewriting -- A Formal Language Theoretic
  		  Perspective on Concurrent Systems}},
  month = oct,
  year = {2009}
}

publications

Drafts/Preprints

Conference papers

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

Journal articles

Theses

Software