Search Results

Documents authored by Totzke, Patrick

Document
DOI: 10.4230/LIPIcs.CONCUR.2024.13
The Power of Counting Steps in Quantitative Games

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

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

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 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.
Cite as

Sougata Bose, Rasmus Ibsen-Jensen, David Purser, Patrick Totzke, and Pierre Vandenhove. The Power of Counting Steps in Quantitative Games. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2024.13,
  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 =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  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},
  annote =	{Keywords: Games on graphs, Markov strategies, quantitative objectives, infinite-state systems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.18
History-Deterministic Vector Addition Systems

Authors: Sougata Bose, David Purser, and Patrick Totzke

Published in: LIPIcs, Volume 279, 34th International Conference on Concurrency Theory (CONCUR 2023)

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 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 ε-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.
Cite as

Sougata Bose, David Purser, and Patrick Totzke. History-Deterministic Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2023.18,
  author =	{Bose, Sougata and Purser, David and Totzke, Patrick},
  title =	{{History-Deterministic Vector Addition Systems}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  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/entities/document/10.4230/LIPIcs.CONCUR.2023.18},
  URN =		{urn:nbn:de:0030-drops-190120},
  doi =		{10.4230/LIPIcs.CONCUR.2023.18},
  annote =	{Keywords: Vector Addition Systems, History-determinism, Good-for Games}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.14
History-Deterministic Timed Automata

Authors: Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
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 automata states.
Cite as

Thomas A. Henzinger, Karoliina Lehtinen, and Patrick Totzke. History-Deterministic Timed Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 14:1-14:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{henzinger_et_al:LIPIcs.CONCUR.2022.14,
  author =	{Henzinger, Thomas A. and Lehtinen, Karoliina and Totzke, Patrick},
  title =	{{History-Deterministic Timed Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{14:1--14:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.14},
  URN =		{urn:nbn:de:0030-drops-170778},
  doi =		{10.4230/LIPIcs.CONCUR.2022.14},
  annote =	{Keywords: Timed Automata, History-determinism, Good-for-games, fair simulation, synthesis}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.47
HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete

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

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

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 complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is Σ₁¹-complete and HyperCTL* satisfiability is Σ₁²-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove Σ₁²-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 Π₁¹-complete.
Cite as

Marie Fortin, Louwe B. Kuijer, Patrick Totzke, and Martin Zimmermann. HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 47:1-47:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{fortin_et_al:LIPIcs.MFCS.2021.47,
  author =	{Fortin, Marie and Kuijer, Louwe B. and Totzke, Patrick and Zimmermann, Martin},
  title =	{{HyperLTL Satisfiability Is \Sigma₁¹-Complete, HyperCTL* Satisfiability Is \Sigma₁²-Complete}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  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/entities/document/10.4230/LIPIcs.MFCS.2021.47},
  URN =		{urn:nbn:de:0030-drops-144870},
  doi =		{10.4230/LIPIcs.MFCS.2021.47},
  annote =	{Keywords: HyperLTL, HyperCTL*, Satisfiability, Analytical Hierarchy}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2021.11
Transience in Countable MDPs

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

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract
The Transience 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 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.
Cite as

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Transience in Countable MDPs. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 11:1-11:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2021.11,
  author =	{Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title =	{{Transience in Countable MDPs}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  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/entities/document/10.4230/LIPIcs.CONCUR.2021.11},
  URN =		{urn:nbn:de:0030-drops-143881},
  doi =		{10.4230/LIPIcs.CONCUR.2021.11},
  annote =	{Keywords: Markov decision processes, Parity, Transience}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.39
Strategy Complexity of Parity Objectives in Countable MDPs

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

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

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 ε-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 ε-optimal or optimal strategies. In particular, 1-bit Markov strategies are necessary and sufficient for ε-optimal (resp. optimal) strategies for general parity objectives.
Cite as

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy Complexity of Parity Objectives in Countable MDPs. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 39:1-39:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.CONCUR.2020.39,
  author =	{Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title =	{{Strategy Complexity of Parity Objectives in Countable MDPs}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  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/entities/document/10.4230/LIPIcs.CONCUR.2020.39},
  URN =		{urn:nbn:de:0030-drops-128513},
  doi =		{10.4230/LIPIcs.CONCUR.2020.39},
  annote =	{Keywords: Markov decision processes, Parity objectives, Levy’s zero-one law}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.47
Parametrized Universality Problems for One-Counter Nets

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

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

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) 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 variants 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.
Cite as

Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized Universality Problems for One-Counter Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 47:1-47:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.47,
  author =	{Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},
  title =	{{Parametrized Universality Problems for One-Counter Nets}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  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/entities/document/10.4230/LIPIcs.CONCUR.2020.47},
  URN =		{urn:nbn:de:0030-drops-128592},
  doi =		{10.4230/LIPIcs.CONCUR.2020.47},
  annote =	{Keywords: Counter net, VASS, Unambiguous Automata, Universality}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.74
Optimally Resilient Strategies in Pushdown Safety Games

Authors: Daniel Neider, Patrick Totzke, and Martin Zimmermann

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

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 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.
Cite as

Daniel Neider, Patrick Totzke, and Martin Zimmermann. Optimally Resilient Strategies in Pushdown Safety Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 74:1-74:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{neider_et_al:LIPIcs.MFCS.2020.74,
  author =	{Neider, Daniel and Totzke, Patrick and Zimmermann, Martin},
  title =	{{Optimally Resilient Strategies in Pushdown Safety Games}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  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}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.74},
  URN =		{urn:nbn:de:0030-drops-127432},
  doi =		{10.4230/LIPIcs.MFCS.2020.74},
  annote =	{Keywords: Controller Synthesis, Infinite Games, Resilient Strategies, Pushdown Games}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.ICALP.2020.3
How to Play in Infinite MDPs (Invited Talk)

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

Published in: LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)

Abstract
Markov decision processes (MDPs) are a standard model for dynamic systems that exhibit both stochastic and nondeterministic behavior. For MDPs with finite state space it is known that for a wide range of objectives there exist optimal strategies that are memoryless and deterministic. In contrast, if the state space is infinite, optimal strategies may not exist, and optimal or ε-optimal strategies may require (possibly infinite) memory. In this paper we consider qualitative objectives: reachability, safety, (co-)Büchi, and other parity objectives. We aim at giving an introduction to a collection of techniques that allow for the construction of strategies with little or no memory in countably infinite MDPs.
Cite as

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, Patrick Totzke, and Dominik Wojtczak. How to Play in Infinite MDPs (Invited Talk). In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 3:1-3:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.ICALP.2020.3,
  author =	{Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick and Wojtczak, Dominik},
  title =	{{How to Play in Infinite MDPs}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  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/entities/document/10.4230/LIPIcs.ICALP.2020.3},
  URN =		{urn:nbn:de:0030-drops-124103},
  doi =		{10.4230/LIPIcs.ICALP.2020.3},
  annote =	{Keywords: Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.15
Timed Basic Parallel Processes

Authors: Lorenzo Clemente, Piotr Hofman, and Patrick Totzke

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

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 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.
Cite as

Lorenzo Clemente, Piotr Hofman, and Patrick Totzke. Timed Basic Parallel Processes. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.CONCUR.2019.15,
  author =	{Clemente, Lorenzo and Hofman, Piotr and Totzke, Patrick},
  title =	{{Timed Basic Parallel Processes}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.15},
  URN =		{urn:nbn:de:0030-drops-109171},
  doi =		{10.4230/LIPIcs.CONCUR.2019.15},
  annote =	{Keywords: Timed Automata, Petri Nets}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.119
Büchi Objectives in Countable MDPs (Track B: Automata, Logic, Semantics, and Theory of Programming)

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

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
We study countably infinite Markov decision processes with Büchi objectives, which ask to visit a given subset F of states infinitely often. A question left open by T.P. Hill in 1979 [Theodore Preston Hill, 1979] is whether there always exist epsilon-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.
Cite as

Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Büchi Objectives in Countable MDPs (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 119:1-119:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{kiefer_et_al:LIPIcs.ICALP.2019.119,
  author =	{Kiefer, Stefan and Mayr, Richard and Shirmohammadi, Mahsa and Totzke, Patrick},
  title =	{{B\"{u}chi Objectives in Countable MDPs}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{119:1--119:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.119},
  URN =		{urn:nbn:de:0030-drops-106959},
  doi =		{10.4230/LIPIcs.ICALP.2019.119},
  annote =	{Keywords: Markov decision processes}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2018.6
Universal Safety for Timed Petri Nets is PSPACE-complete

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

Published in: LIPIcs, Volume 118, 29th International Conference on Concurrency Theory (CONCUR 2018)

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 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.
Cite as

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Radu Ciobanu, Richard Mayr, and Patrick Totzke. Universal Safety for Timed Petri Nets is PSPACE-complete. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 6:1-6:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{abdulla_et_al:LIPIcs.CONCUR.2018.6,
  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 =	{29th International Conference on Concurrency Theory (CONCUR 2018)},
  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},
  editor =	{Schewe, Sven and Zhang, Lijun},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2018.6},
  URN =		{urn:nbn:de:0030-drops-95447},
  doi =		{10.4230/LIPIcs.CONCUR.2018.6},
  annote =	{Keywords: timed networks, safety checking, Petri nets, coverability}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.105
A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One

Authors: Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

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 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.
Cite as

Stefan Göller, Christoph Haase, Ranko Lazic, and Patrick Totzke. A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 105:1-105:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.ICALP.2016.105,
  author =	{G\"{o}ller, Stefan and Haase, Christoph and Lazic, Ranko and Totzke, Patrick},
  title =	{{A Polynomial-Time Algorithm for Reachability in Branching VASS in Dimension One}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{105:1--105:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.105},
  URN =		{urn:nbn:de:0030-drops-62409},
  doi =		{10.4230/LIPIcs.ICALP.2016.105},
  annote =	{Keywords: branching vector addition systems, reachability, coverability, boundedness}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.515
Simulation Over One-counter Nets is PSPACE-Complete

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

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

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.
Cite as

Piotr Hofman, Slawomir Lasota, Richard Mayr, and Patrick Totzke. Simulation Over One-counter Nets is PSPACE-Complete. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 515-526, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{hofman_et_al:LIPIcs.FSTTCS.2013.515,
  author =	{Hofman, Piotr and Lasota, Slawomir and Mayr, Richard and Totzke, Patrick},
  title =	{{Simulation Over One-counter Nets is PSPACE-Complete}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{515--526},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.515},
  URN =		{urn:nbn:de:0030-drops-43970},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.515},
  annote =	{Keywords: Simulation preorder; one-counter nets; complexity}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact