We provide a new algebraic technique to solve the sequential flow problem in polynomial space. The task is to maximize the flow through a graph where edge capacities can be changed over time by choosing a sequence of capacity labelings from a given finite set.
Our method is based on a novel factorization theorem for finite semigroups that, applied to a suitable flow semigroup, allows to derive small witnesses. This generalizes to multiple in/output vertices, as well as regular constraints.
@misc{gmt2025,title={Optimal Sequential Flows},author={Gimbert, Hugo and Mascle, Corto and Totzke, Patrick},year={2025},}
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL^* is Even Harder
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 also prove this bound to be tight. Furthermore, we prove that both countable and finitely-branching satisfiability for HyperCTL* are as hard as truth in second-order arithmetic, i.e., still highly undecidable.
Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is \(\Pi_1^1\)-complete.
@article{fktz2025,title={HyperLTL Satisfiability Is Highly Undecidable,
HyperCTL$^*$ is Even Harder},author={Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},url={https://lmcs.episciences.org/11608},doi={10.46298/lmcs-21(1:3)2025},journal={Logical Methods in Computer Science },issn={1860-5974},volume={Volume 21, Issue 1},eid={3},year={2025},month=jan,}
History-deterministic automata are those in which nondeterministic choices can be correctly resolved stepwise: there is a strategy to select a continuation of a run given the next input letter so that if the overall input word admits some accepting run, then the constructed run is also accepting.
Motivated by checking qualitative properties in probabilistic verification, we consider the setting where the resolver strategy can randomize and only needs to succeed with lower-bounded probability. We study the expressiveness of such stochastically-resolvable automata as well as consider the decision questions of whether a given automaton has this property. In particular, we show that it is undecidable to check if a given NFA is \(λ\)-stochastically resolvable. This problem is decidable for finitely-ambiguous automata. We also present complexity upper and lower bounds for several well-studied classes of automata for which this problem remains decidable.
@inproceedings{ppstty2025,title={{Resolving Nondeterminism by Chance}},author={Paul, Soumyajit and Purser, David and Schewe, Sven and Tang, Qiyi and Totzke, Patrick and Yen, Di-De},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={32:1--32:22},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-389-8},issn={1868-8969},year={2025},volume={348},editor={Bouyer, Patricia and van de Pol, Jaco},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.32},urn={urn:nbn:de:0030-drops-239822},doi={10.4230/LIPIcs.CONCUR.2025.32},month=aug,}
Temporal graphs extend ordinary graphs with discrete time that affects the availability of edges. We consider solving games played on temporal graphs where one player aims to explore the graph, i.e., visit all vertices. The complexity depends majorly on two factors: the presence of an adversary and how edge availability is specified.
We demonstrate that on static graphs, where edges are always available, solving explorability games is just as hard as solving reachability games. In contrast, on temporal graphs, the complexity of explorability coincides with generalized reachability (NP-complete for one-player and PSPACE- complete for two player games). We further show that if temporal graphs are given symbolically, even one-player reachability and thus explorability and generalized reachability games are PSPACE-hard. For one player, all these are also solvable in PSPACE and for two players, they are in PSPACE, EXP and EXP, respectively.
@inproceedings{abt2025,title={{Temporal Explorability Games}},author={Austin, Pete and Bose, Sougata and Mazzocchi, Nicolas and Totzke, Patrick},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={7:1--7:17},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-389-8},issn={1868-8969},year={2025},volume={348},editor={Bouyer, Patricia and van de Pol, Jaco},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2025.7},urn={urn:nbn:de:0030-drops-239575},doi={10.4230/LIPIcs.CONCUR.2025.7},month=aug,}
Strategy Complexity of Büchi and Transience Objectives in Concurrent Stochastic Games
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: \varepsilon-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 \varepsilon-optimal Max strategies for the Transience objective alone (which is only meaningful in infinite graphs) can be memoryless.
@inproceedings{kmst2025a,author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},title={Strategy Complexity of B\"{u}chi and Transience Objectives
in Concurrent Stochastic Games},year={2025},month=jul,isbn={9798400719431},publisher={Association for Computing Machinery},address={New York, NY, USA},url={https://doi.org/10.1145/3736252.3742560},doi={10.1145/3736252.3742560},booktitle={ACM Conference on Economics and Computation},pages={390–409},numpages={20},location={Stanford University, Stanford, CA, USA}}
The random population control decision problem asks for the existence of a controller capable of gathering almost-surely a whole population of identical finite-state agents simultaneously in a final state. The controller must be able to satisfy this requirement however large the population, provided that it is finite. The problem was previously known to be decidable and EXPTIME-hard. This paper tackles the exact complexity: the problem is EXPTIME-complete.
@misc{gmt2024,title={Optimally Controlling a Random Population},author={Gimbert, Hugo and Mascle, Corto and Totzke, Patrick},year={2024},}
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.
@article{bhlst2023,title={History-deterministic Timed Automata},author={Bose, Sougata and Henzinger, Thomas A. and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick},url={https://lmcs.episciences.org/14429},doi={10.46298/lmcs-20(4:1)2024},journal={Logical Methods in Computer Science },volume={{Volume 20, Issue 4}},year={2024},month=oct,}
Strategy Complexity of Reachability in Countable Stochastic 2-Player Games
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.
@article{kmst2022,title={Strategy Complexity of Reachability in Countable
Stochastic 2-Player Games},author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},journal={Dynamic Games and Applications},year={2024},month=sep,doi={10.1007/s13235-024-00575-6},}
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.
@inproceedings{biptv2024,author={Bose, Sougata and Ibsen-Jensen, Rasmus and Purser, David and Totzke, Patrick and Vandenhove, Pierre},title={{The Power of Counting Steps in Quantitative Games}},booktitle={International Conference on Concurrency Theory (CONCUR)},pages={13:1--13:18},series={Leibniz International Proceedings in Informatics
(LIPIcs)},isbn={978-3-95977-339-3},issn={1868-8969},year={2024},month=aug,volume={311},editor={Majumdar, Rupak and Silva, Alexandra},publisher={Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},address={Dagstuhl, Germany},url={https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.13},urn={urn:nbn:de:0030-drops-207852},doi={10.4230/LIPIcs.CONCUR.2024.13},}
Bounded-Memory Strategies in Partial-Information Games
Sougata Bose, Rasmus Ibsen-Jensen, and Patrick Totzke
In ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2024
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}}\).
@inproceedings{bit2024,title={Bounded-Memory Strategies in Partial-Information Games},author={Bose, Sougata and Ibsen{-}Jensen, Rasmus and Totzke, Patrick},booktitle={ACM/IEEE Symposium on Logic in Computer Science (LICS)},doi={10.1145/3661814.3662096},year={2024},month=jul,}
Memoryless Strategies in Stochastic Reachability Games
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.
@inbook{kmst2024,title={Memoryless Strategies in Stochastic Reachability Games},author={Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},year={2024},month=mar,doi={10.1007/978-3-031-56222-8_13},editor={Kiefer, Stefan and K{\v{r}}et{\'i}nsk{\'y}, Jan and Ku{\v{c}}era, Anton{\'i}n},booktitle={Taming the Infinities of Concurrency},journal={Lecture Notes in Computer Science},publisher={Springer Nature Switzerland},address={Cham},pages={225--242},isbn={978-3-031-56222-8},url={https://doi.org/10.1007/978-3-031-56222-8_13},}
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},month=apr,url={https://doi.org/10.1007/978-3-031-57228-9\_5},doi={10.1007/978-3-031-57228-9\_5},}
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},}
@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
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)},}
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},}
@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
The Reachability Problem for Two-Dimensional Vector Addition Systems with States
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},}
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.
There exist uniformly \(\varepsilon\)-optimal MD strategies (memoryless deterministic) for Transient, even in infinitely branching MDPs.
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.
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},teaser={https://stream.liv.ac.uk/xrvdpjs5},}
HyperLTL Satisfiability is \(\Sigma_1^1\)-complete, HyperCTL* Satisfiability is \(\Sigma_1^2\)-complete
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
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
@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},}
@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
@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
@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},teaser={ https://www.youtube.com/watch?v=ZIU0Ocdb7vs},}
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},}
@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},}
@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
@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
What Makes Petri Nets Harder to Verify: Stack or Data?
@inbook{lt2017,author={Lazi{\'c}, Ranko and Totzke, Patrick},title={{What Makes Petri Nets Harder to Verify: Stack or Data?}},editor={Gibson-Robinson, Thomas and Hopcroft, Philippa and Lazi{\'{c}}, Ranko},booktitle={Concurrency, Security, and Puzzles},publisher={Springer International Publishing},address={Cham},journal={Lecture Notes in Computer Science},volume={10160},number={1},pages={144--161},year={2017},doi={10.1007/978-3-319-51046-0_8},}
@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},}
@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},}
@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
Branching-Time Model Checking Gap-Order Constraint Systems
@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},}
@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},}
Reachability in Two-Dimensional Unary Vector Addition Systems with States is NL-Complete
@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
@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
@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
@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
@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},}
@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)},}
@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},}
@phdthesis{t2014,author={Totzke, Patrick},school={University of Edinburgh},title={{Inclusion Problems for One-Counter Systems}},month=apr,year={2014},}
2013
Simulation Over One-Counter Nets is PSPACE-Complete
@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
@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
@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
@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},}
2009
Properties of Multiset Language Classes Defined by Multiset Pushdown Automata
@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},}
@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},}
Multiset Rewriting – A Formal Language Theoretic Perspective on Concurrent Systems
@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},}