Showing 1–34 of 34 results for author: Totzke, P

The Power of Counting Steps in Quantitative Games

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

Abstract: We study deterministic 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… ▽ More We study deterministic 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. △ Less

Submitted 25 June, 2024; originally announced June 2024.

Comments: Extended version of a CONCUR 2024 paper

Bounded-Memory Strategies in Partial-Information Games

Authors: Sougata Bose, Rasmus Ibsen-Jensen, Patrick Totzke

Abstract: 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 $ε$-optimally, or form $ε$-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 s… ▽ More 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 $ε$-optimally, or form $ε$-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, $ε\ge 0$ and bound $b$, there exists an $ε$-Nash equilibrium in which all strategies use at most $b$ memory modes. For given $ε>0$, finding an $ε$-Nash equilibrium with respect to $b$-bounded strategies can be done in $FN[NP]$. Similarly for 2-player zero-sum games, finding a $b$-bounded strategy that, against all $b$-bounded opponent strategies, guarantees an outcome within $ε$ of a given value, can be done in $FNP[NP]$. Our constructions apply to parity objectives with 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, one can approximate ordinary zero-sum values (without restricting admissible strategies) in $FNP[NP]$. △ Less

Submitted 15 May, 2024; originally announced May 2024.

Strategy Complexity of Büchi Objectives in Concurrent Stochastic Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: 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 n… ▽ More 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. △ Less

Submitted 23 April, 2024; originally announced April 2024.

MSC Class: 91A35; 91A15 ACM Class: G.3

Memoryless Strategies in Stochastic Reachability Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: 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… ▽ More 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. △ Less

Submitted 24 January, 2024; originally announced January 2024.

Parity Games on Temporal Graphs

Authors: Pete Austin, Sougata Bose, Patrick Totzke

Abstract: 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… ▽ More 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. △ Less

Submitted 28 January, 2024; v1 submitted 19 October, 2023; originally announced October 2023.

Handling of Past and Future with Phenesthe+

Authors: Manolis Pitsikalis, Alexei Lisitsa, Patrick Totzke

Abstract: Writing temporal logic formulae for properties that combine instantaneous events with overlap** temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new temporal logic with intuitive temporal modalities specifically tailored for the representation of both instantaneous and durative phenomena. We also provided an im… ▽ More Writing temporal logic formulae for properties that combine instantaneous events with overlap** temporal phenomena of some duration is difficult in classical temporal logics. To address this issue, in previous work we introduced a new temporal logic with intuitive temporal modalities specifically tailored for the representation of both instantaneous and durative phenomena. We also provided an implementation of a complex event processing system, Phenesthe, based on this logic, that has been applied and tested on a real maritime surveillance scenario. In this work, we extend our temporal logic with two extra modalities to increase its expressive power for handling future formulae. We compare the expressive power of different fragments of our logic with Linear Temporal Logic and dyadic first-order logic. Furthermore, we define correctness criteria for stream processors that use our language. Last but not least, we evaluate empirically the performance of Phenesthe+, our extended implementation, and show that the increased expressive power does not affect efficiency significantly. △ Less

Submitted 2 October, 2023; originally announced October 2023.

Comments: In Proceedings GandALF 2023, arXiv:2309.17318

ACM Class: F.4.1; I.2.4

Journal ref: EPTCS 390, 2023, pp. 33-49

History-deterministic Vector Addition Systems

Authors: Sougata Bose, David Purser, Patrick Totzke

Abstract: 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. 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 t… ▽ More 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. 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, and with and without $\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 a VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable. △ Less

Submitted 10 July, 2023; v1 submitted 3 May, 2023; originally announced May 2023.

Comments: This is the full version of a paper published in CONCUR 2023

History-deterministic Timed Automata

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

Abstract: 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 with… ▽ More 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 safety/reachability TA. For history-deterministic TA with arbitrary parity acceptance, we show that timed universality, inclusion, and synthesis all remain decidable and are EXPTIME-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. △ Less

Submitted 9 November, 2023; v1 submitted 6 April, 2023; originally announced April 2023.

HyperLTL Satisfiability Is Highly Undecidable, HyperCTL* is Even Harder

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Abstract: 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… ▽ More 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 $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_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 $Π_1^1$-complete. △ Less

Submitted 30 March, 2023; v1 submitted 29 March, 2023; originally announced March 2023.

Comments: Extended version of a paper presented at MFCS 2021 and archived as arXiv:2105.04176

Strategy Complexity of Reachability in Countable Stochastic 2-Player Games

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: 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 the size of the players' action sets and on whether one requires strategies that are uniform (i.e., independent of the start state). Our main result is that $\varepsilon$-… ▽ More 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 the size of the players' action sets 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 require infinite memory if Minimizer is allowed infinite action sets. This lower bound holds even under very strong restrictions. Even in the special case of infinitely branching turn-based reachability games, even if all states allow 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 (i.e., memoryless) uniformly $\varepsilon$-optimal strategies even in the special case of finite action sets or in finitely branching turn-based games. On the other hand, in games with finite action sets, there always exists a uniformly $\varepsilon$-optimal Maximizer strategy that uses just one bit of public memory. △ Less

Submitted 2 July, 2024; v1 submitted 22 March, 2022; originally announced March 2022.

MSC Class: 91A35; 91A15 ACM Class: G.3

HyperLTL Satisfiability is $Σ_1^1$-complete, HyperCTL* Satisfiability is $Σ_1^2$-complete

Authors: Marie Fortin, Louwe B. Kuijer, Patrick Totzke, Martin Zimmermann

Abstract: 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… ▽ More 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 $Σ_1^1$-complete and HyperCTL* satisfiability is $Σ_1^2$-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove $Σ_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 $Π_1^1$-complete. △ Less

Submitted 10 May, 2021; originally announced May 2021.

MSC Class: 03D35 ACM Class: F.4.1; F.3.1

Simple Stochastic Games with Almost-Sure Energy-Parity Objectives are in NP and coNP

Authors: Richard Mayr, Sven Schewe, Patrick Totzke, Dominik Wojtczak

Abstract: 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 probabil… ▽ More 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 \cap coNP$. The same holds for checking if such a $k$ exists and if a given $k$ is minimal. △ Less

Submitted 18 January, 2021; originally announced January 2021.

Transience in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: The Transience objective is not to visit any state infinitely often. While this is not possible in 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 Transience in countably infinite MDPs. 1. There exist uniformly $ε$-optimal MD strategies (memoryless deterministic) for T… ▽ More The Transience objective is not to visit any state infinitely often. While this is not possible in 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 Transience in countably infinite MDPs. 1. There exist uniformly $ε$-optimal MD strategies (memoryless deterministic) for Transience, even in infinitely branching MDPs. 2. Optimal strategies for Transience 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., $ε$-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. △ Less

Submitted 4 July, 2021; v1 submitted 26 December, 2020; originally announced December 2020.

Strategy Complexity of Parity Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of $\varepsilon$-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov st… ▽ More We study countably infinite MDPs with parity objectives. Unlike in finite MDPs, optimal strategies need not exist, and may require infinite memory if they do. We provide a complete picture of the exact strategy complexity of $\varepsilon$-optimal strategies (and optimal strategies, where they exist) for all subclasses of parity objectives in the Mostowski hierarchy. Either MD-strategies, Markov strategies, or 1-bit Markov strategies are necessary and sufficient, depending on the number of colors, the branching degree of the MDP, and whether one considers $\varepsilon$-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for $\varepsilon$-optimal (resp. optimal) strategies for general parity objectives. △ Less

Submitted 7 July, 2020; originally announced July 2020.

Comments: This is the full version of a paper presented at CONCUR 2020

Parametrized Universality Problems for One-Counter Nets

Authors: Shaull Almagor, Udi Boker, Piotr Hofman, Patrick Totzke

Abstract: We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1… ▽ More We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) Does there exist an initial counter value that makes the language universal? 2) Does there exist a sufficiently high ceiling so that the bounded language is universal? Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized problems seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet. △ Less

Submitted 4 July, 2020; v1 submitted 7 May, 2020; originally announced May 2020.

Optimally Resilient Strategies in Pushdown Safety Games

Authors: Daniel Neider, Patrick Totzke, Martin Zimmermann

Abstract: Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that co… ▽ More Infinite-duration games with disturbances extend the classical framework of infinite-duration games, which captures the reactive synthesis problem, with a discrete measure of resilience against non-antagonistic external influence. This concerns events where the observed system behavior differs from the intended one prescribed by the controller. For games played on finite arenas it is known that computing optimally resilient strategies only incurs a polynomial overhead over solving classical games. This paper studies safety games with disturbances played on infinite arenas induced by pushdown systems. We show how to compute optimally resilient strategies in triply-exponential time. For the subclass of safety games played on one-counter configuration graphs, we show that determining the degree of resilience of the initial configuration is PSPACE-complete and that optimally resilient strategies can be computed in doubly-exponential time. △ Less

Submitted 8 July, 2020; v1 submitted 10 December, 2019; originally announced December 2019.

Controlling a Random Population is EXPTIME-hard

Authors: Corto Mascle, Mahsa Shirmohammadi, Patrick Totzke

Abstract: Bertrand et al. [1] (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 co… ▽ More Bertrand et al. [1] (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. △ Less

Submitted 13 September, 2019; originally announced September 2019.

Timed Basic Parallel Processes

Authors: Lorenzo Clemente, Piotr Hofman, Patrick Totzke

Abstract: Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with… ▽ More Timed basic parallel processes (TBPP) extend communication-free Petri nets (aka. BPP or commutative context-free grammars) by a global notion of time. TBPP can be seen as an extension of timed automata (TA) with context-free branching rules, and as such may be used to model networks of independent timed automata with process creation. We show that the coverability and reachability problems (with unary encoded target multiplicities) are PSPACE-complete and EXPTIME-complete, respectively. For the special case of 1-clock TBPP, both are NP-complete and hence not more complex than for untimed BPP. This contrasts with known super-Ackermannian-completeness and undecidability results for general timed Petri nets. As a result of independent interest, and basis for our NP upper bounds, we show that the reachability relation of 1-clock TA can be expressed by a formula of polynomial size in the existential fragment of linear arithmetic, which improves on recent results from the literature. △ Less

Submitted 8 July, 2019; v1 submitted 2 July, 2019; originally announced July 2019.

Büchi Objectives in Countable MDPs

Authors: Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke

Abstract: We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist $\varepsilon$-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question b… ▽ More We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset of states infinitely often. A question left open by T.P. Hill in 1979 is whether there always exist $\varepsilon$-optimal Markov strategies, i.e., strategies that base decisions only on the current state and the number of steps taken so far. We provide a negative answer to this question by constructing a non-trivial counterexample. On the other hand, we show that Markov strategies with only 1 bit of extra memory are sufficient. △ Less

Submitted 30 April, 2019; v1 submitted 25 April, 2019; originally announced April 2019.

Comments: full version of an ICALP'19 paper. This update only fixes some typesetting issues

Universal Safety for Timed Petri Nets is PSPACE-complete

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

Abstract: A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible re… ▽ More A timed network consists of an arbitrary number of initially identical 1-clock timed automata, interacting via hand-shake communication. In this setting there is no unique central controller, since all automata are initially identical. We consider the universal safety problem for such controller-less timed networks, i.e., verifying that a bad event (enabling some given transition) is impossible regardless of the size of the network. This universal safety problem is dual to the existential coverability problem for timed-arc Petri nets, i.e., does there exist a number $m$ of tokens, such that starting with $m$ tokens in a given place, and none in the other places, some given transition is eventually enabled. We show that these problems are PSPACE-complete. △ Less

Submitted 21 June, 2018; originally announced June 2018.

ACM Class: F.1.1

MDPs with Energy-Parity Objectives

Authors: Richard Mayr, Sven Schewe, Patrick Totzke, Dominik Wojtczak

Abstract: Energy-parity objectives combine $ω$-regular with quantitative objectives of reward MDPs. The controller needs to avoid to run out of energy while satisfying a parity objective. We refute the common belief that, if an energy-parity objective holds almost-surely, then this can be realised by some finite memory strategy. We provide a surprisingly simple counterexample that only uses coBüchi condit… ▽ More Energy-parity objectives combine $ω$-regular with quantitative objectives of reward MDPs. The controller needs to avoid to run out of energy while satisfying a parity objective. We refute the common belief that, if an energy-parity objective holds almost-surely, then this can be realised by some finite memory strategy. We provide a surprisingly simple counterexample that only uses coBüchi conditions. We introduce the new class of bounded (energy) storage objectives that, when combined with parity objectives, preserve the finite memory property. Based on these, we show that almost-sure and limit-sure energy-parity objectives, as well as almost-sure and limit-sure storage parity objectives, are in $\mathit{NP}\cap \mathit{coNP}$ and can be solved in pseudo-polynomial time for energy-parity MDPs. △ Less

Submitted 18 April, 2017; v1 submitted 10 January, 2017; originally announced January 2017.

Linear Combinations of Unordered Data Vectors

Authors: Piotr Hofman, Jérôme Leroux, Patrick Totzke

Abstract: Data vectors generalise finite multisets: they are finitely supported functions into a commutative monoid. We study the question if a given data vector can be expressed as a finite sum of others, only assuming that 1) the domain is countable and 2) the given set of base vectors is finite up to permutations of the domain. Based on a succinct representation of the involved permutations as integer… ▽ More Data vectors generalise finite multisets: they are finitely supported functions into a commutative monoid. We study the question if a given data vector can be expressed as a finite sum of others, only assuming that 1) the domain is countable and 2) the given set of base vectors is finite up to permutations of the domain. Based on a succinct representation of the involved permutations as integer linear constraints, we derive that positive instances can be witnessed in a bounded subset of the domain. For data vectors over a group we moreover study when a data vector is reversible, that is, if its inverse is expressible using only nonnegative coefficients. We show that if all base vectors are reversible then the expressibility problem reduces to checking membership in finitely generated subgroups. Moreover, checking reversibility also reduces to such membership tests. These questions naturally appear in the analysis of counter machines extended with unordered data: namely, for data vectors over $(\mathbb{Z}^d,+)$ expressibility directly corresponds to checking state equations for Coloured Petri nets where tokens can only be tested for equality. We derive that in this case, expressibility is in NP, and in P for reversible instances. These upper bounds are tight: they match the lower bounds for standard integer vectors (over singleton domains). △ Less

Submitted 5 October, 2016; originally announced October 2016.

ACM Class: F.1.1

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

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

Abstract: Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS… ▽ More Branching VASS (BVASS) generalise vector addition systems with states by allowing for special branching transitions that can non-deterministically distribute a counter value between two control states. A run of a BVASS consequently becomes a tree, and reachability is to decide whether a given configuration is the root of a reachability tree. This paper shows P-completeness of reachability in BVASS in dimension one, the first decidability result for reachability in a subclass of BVASS known so far. Moreover, we show that coverability and boundedness in BVASS in dimension one are P-complete as well. △ Less

Submitted 6 May, 2016; v1 submitted 17 February, 2016; originally announced February 2016.

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

Authors: Matthias Englert, Ranko Lazić, Patrick Totzke

Abstract: Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish t… ▽ More Blondin et al. showed at LICS 2015 that two-dimensional vector addition systems with states have reachability witnesses of length exponential in the number of states and polynomial in the norm of vectors. The resulting guess-and-verify algorithm is optimal (PSPACE), but only if the input vectors are given in binary. We answer positively the main question left open by their work, namely establish that reachability witnesses of pseudo-polynomial length always exist. Hence, when the input vectors are given in unary, the improved guess-and-verify algorithm requires only logarithmic space. △ Less

Submitted 6 May, 2016; v1 submitted 1 February, 2016; originally announced February 2016.

ACM Class: F.1.1

Simulation Problems Over One-Counter Nets

Authors: Piotr Hofman, Slawomir Lasota, Richard Mayr, Patrick Totzke

Abstract: One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are PSPACE-complete. One-counter nets (OCN) are finite automata equipped with a counter that can store non-negative integer values, and that cannot be tested for zero. Equivalently, these are exactly 1-dimensional vector addition systems with states. We show that both strong and weak simulation preorder on OCN are PSPACE-complete. △ Less

Submitted 10 March, 2016; v1 submitted 1 February, 2016; originally announced February 2016.

Journal ref: Logical Methods in Computer Science, Volume 12, Issue 1 (March 14, 2016) lmcs:1629

On Boundedness Problems for Pushdown Vector Addition Systems

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

Abstract: We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability set for this model can be refined into two decision problems that ask if infinitely many counter values or stack configurations are reachable, respectively. Counter boundedness seems to be the more intricate problem. We… ▽ More We study pushdown vector addition systems, which are synchronized products of pushdown automata with vector addition systems. The question of the boundedness of the reachability set for this model can be refined into two decision problems that ask if infinitely many counter values or stack configurations are reachable, respectively. Counter boundedness seems to be the more intricate problem. We show decidability in exponential time for one-dimensional systems. The proof is via a small witness property derived from an analysis of derivation trees of grammar-controlled vector addition systems. △ Less

Submitted 27 July, 2015; originally announced July 2015.

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

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

Abstract: Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new… ▽ More Does the trace language of a given vector addition system (VAS) intersect with a given context-free language? This question lies at the heart of several verification questions involving recursive programs with integer parameters. In particular, it is equivalent to the coverability problem for VAS that operate on a pushdown stack. We show decidability in dimension one, based on an analysis of a new model called grammar-controlled vector addition systems. △ Less

Submitted 29 April, 2015; v1 submitted 13 March, 2015; originally announced March 2015.

ACM Class: F.4.2; F.4.3

Scaled tree fractals do not strictly self-assemble

Authors: Kimberly Barth, David Furcy, Scott M. Summers, Paul Totzke

Abstract: In this paper, we show that any scaled-up version of any discrete self-similar {\it tree} fractal does not strictly self-assemble, at any temperature, in Winfree's abstract Tile Assembly Model. In this paper, we show that any scaled-up version of any discrete self-similar {\it tree} fractal does not strictly self-assemble, at any temperature, in Winfree's abstract Tile Assembly Model. △ Less

Submitted 11 November, 2014; originally announced November 2014.

Comments: 13 pages, 3 figures, Appeared in the Proceedings of UCNC-2014, pp 27-39; Unconventional Computation and Natural Computation - 13th International Conference, UCNC 2014, London, ON, Canada, July 14-18, 2014, Springer Lecture Notes in Computer Science ISBN 978-3-319-08122-9

Infinite-State Energy Games

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

Abstract: Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induce… ▽ More Energy games are a well-studied class of 2-player turn-based games on a finite graph where transitions are labeled with integer vectors which represent changes in a multidimensional resource (the energy). One player tries to keep the cumulative changes non-negative in every component while the other tries to frustrate this. We consider generalized energy games played on infinite game graphs induced by pushdown automata (modelling recursion) or their subclass of one-counter automata. Our main result is that energy games are decidable in the case where the game graph is induced by a one-counter automaton and the energy is one-dimensional. On the other hand, every further generalization is undecidable: Energy games on one-counter automata with a 2-dimensional energy are undecidable, and energy games on pushdown automata are undecidable even if the energy is one-dimensional. Furthermore, we show that energy games and simulation games are inter-reducible, and thus we additionally obtain several new (un)decidability results for the problem of checking simulation preorder between pushdown automata and vector addition systems. △ Less

Submitted 3 May, 2014; originally announced May 2014.

Comments: 11 pages

Report number: EDI-INF-RR-1419 MSC Class: 91A43 ACM Class: F.3.1

Journal ref: Full version (including proofs) of material presented at CSL-LICS 2014 (Vienna, Austria)

Trace Inclusion for One-Counter Nets Revisited

Authors: Piotr Hofman, Patrick Totzke

Abstract: One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexit… ▽ More One-Counter nets (OCN) consist of a nondeterministic finite control and a single integer counter that cannot be fully tested for zero. They form a natural subclass of both One-Counter Automata, which allow zero-tests and Petri Nets/VASS, which allow multiple such weak counters. The trace inclusion problem has recently been shown to be undecidable for OCN. In this paper, we contrast the complexity of two natural restrictions which imply decidability. First, we show that trace inclusion between an OCN and a deterministic OCN is NL-complete, even with arbitrary binary-encoded initial counter-values as part of the input. Secondly, we show Ackermannian completeness of for the trace universality problem of nondeterministic OCN. This problem is equivalent to checking trace inclusion between a finite and a OCN-process. △ Less

Submitted 19 April, 2015; v1 submitted 21 April, 2014; originally announced April 2014.

Simulation Over One-counter Nets is PSPACE-Complete

Authors: Piotr Hofman, Slawomir Lasota, Richard Mayr, Patrick Totzke

Abstract: One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete. One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with just a weak test for zero. Unlike many other semantic equivalences, strong and weak simulation preorder are decidable for OCN, but the computational complexity was an open problem. We show that both strong and weak simulation preorder on OCN are PSPACE-complete. △ Less

Submitted 23 October, 2013; originally announced October 2013.

Comments: Extended version of material presented at the FST&TCS 2013 conference. 22 pages

Report number: EDI-INF-RR-1418 MSC Class: 68Q45 ACM Class: F.1.1; D.2.4

Branching-Time Model Checking Gap-Order Constraint Systems (Extended Version)

Authors: Richard Mayr, Patrick Totzke

Abstract: We consider the model checking problem for Gap-order Constraint Systems (GCS) w.r.t. the branching-time temporal logic CTL, and in particular its fragments EG and EF. GCS are nondeterministic infinitely branching processes described by evolutions of integer-valued variables, subject to Presburger constraints of the form $x-y\ge k$, where $x$ and $y$ are variables or constants and… ▽ More We consider the model checking problem for Gap-order Constraint Systems (GCS) w.r.t. the branching-time temporal logic CTL, and in particular its fragments EG and EF. GCS are nondeterministic infinitely branching processes described by evolutions of integer-valued variables, subject to Presburger constraints of the form $x-y\ge k$, where $x$ and $y$ are variables or constants and $k\in\mathbb{N}$ is a non-negative constant. We show that EG model checking is undecidable for GCS, while EF is decidable. In particular, this implies the decidability of strong and weak bisimulation equivalence between GCS and finite-state systems. △ Less

Submitted 25 February, 2015; v1 submitted 16 July, 2013; originally announced July 2013.

MSC Class: 03B70; 68Q42 ACM Class: D.2.4; F.1.1; F.3.1

Decidability of Weak Simulation on One-counter Nets

Authors: Piotr Hofman, Richard Mayr, Patrick Totzke

Abstract: One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, an… ▽ More One-counter nets (OCN) are Petri nets with exactly one unbounded place. They are equivalent to a subclass of one-counter automata with only a weak test for zero. We show that weak simulation preorder is decidable for OCN and that weak simulation approximants do not converge at level omega, but only at omega^2. In contrast, other semantic relations like weak bisimulation are undecidable for OCN, and so are weak (and strong) trace inclusion. △ Less

Submitted 15 June, 2014; v1 submitted 15 April, 2013; originally announced April 2013.

Comments: 24 pages

Report number: EDI-INF-RR-1415 MSC Class: 68Q45 ACM Class: F.1.1; D.2.4

Approximating Weak Bisimilarity of Basic Parallel Processes

Authors: Piotr Hofman, Patrick Totzke

Abstract: This paper explores the well known approximation approach to decide weak bisimilarity of Basic Parallel Processes. We look into how different refinement functions can be used to prove weak bisimilarity decidable for certain subclasses. We also show their limitations for the general case. In particular, we show a lower bound of ω \ast ω for the approximants which allow weak steps and a lower bound… ▽ More This paper explores the well known approximation approach to decide weak bisimilarity of Basic Parallel Processes. We look into how different refinement functions can be used to prove weak bisimilarity decidable for certain subclasses. We also show their limitations for the general case. In particular, we show a lower bound of ω \ast ω for the approximants which allow weak steps and a lower bound of ω + ω for the approximants that allow sequences of actions. The former lower bound negatively answers the open question of Jančar and Hirshfeld. △ Less

Submitted 13 August, 2012; originally announced August 2012.

Comments: In Proceedings EXPRESS/SOS 2012, arXiv:1208.2440

ACM Class: F.0

Journal ref: EPTCS 89, 2012, pp. 99-113