arXiv subjects

Patrick Totzke

Publications and source records attributed to Patrick Totzke.

At least 37 records · Page 2Linked to original sources

arXiv2021

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

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.

cs.GT↗

arXiv2020

Optimally Resilient Strategies in Pushdown Safety Games

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.

cs.GT↗

arXiv2020

Strategy Complexity of Parity Objectives in Countable MDPs

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.

cs.LO↗

arXiv2020

Parametrized Universality Problems for One-Counter Nets

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.

cs.FL↗

arXiv2019

Controlling a Random Population is EXPTIME-hard

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.

cs.LO↗

arXiv2019

Timed Basic Parallel Processes

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.

cs.FL↗

arXiv2019

Büchi Objectives in Countable MDPs

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.

math.PR↗

arXiv2018

Universal Safety for Timed Petri Nets is PSPACE-complete

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.

cs.LO↗

arXiv2017

MDPs with Energy-Parity Objectives

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.

cs.LO↗

arXiv2016

Linear Combinations of Unordered Data Vectors

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

cs.LO↗

arXiv2016

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

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.

cs.LO↗

arXiv2016

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

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.

cs.FL↗

arXiv2016

Simulation Problems Over One-Counter Nets

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.

cs.LO↗

arXiv2015

On Boundedness Problems for Pushdown Vector Addition Systems

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.

cs.FL↗

arXiv2015

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

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.

cs.FL↗

arXiv2015

Trace Inclusion for One-Counter Nets Revisited

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.

cs.LO↗

arXiv2015

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

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.

cs.LO↗

arXiv2014

Decidability of Weak Simulation on One-counter Nets

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.

cs.FL↗