Search Results

Documents authored by Zimmermann, Martin

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.31
History-Deterministic Parikh Automata

Authors: Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann

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

Abstract
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run. Thereby, they preserve many of the desirable properties of finite automata. Deterministic Parikh automata are strictly weaker than nondeterministic ones, but enjoy better closure and algorithmic properties. This state of affairs motivates the study of intermediate forms of nondeterminism. Here, we investigate history-deterministic Parikh automata, i.e., automata whose nondeterminism can be resolved on the fly. This restricted form of nondeterminism is well-suited for applications which classically call for determinism, e.g., solving games and composition. We show that history-deterministic Parikh automata are strictly more expressive than deterministic ones, incomparable to unambiguous ones, and enjoy almost all of the closure properties of deterministic automata.
Cite as

Enzo Erlich, Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. History-Deterministic Parikh Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{erlich_et_al:LIPIcs.CONCUR.2023.31,
  author =	{Erlich, Enzo and Guha, Shibashis and Jecker, Isma\"{e}l and Lehtinen, Karoliina and Zimmermann, Martin},
  title =	{{History-Deterministic Parikh Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{31:1--31:16},
  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.31},
  URN =		{urn:nbn:de:0030-drops-190250},
  doi =		{10.4230/LIPIcs.CONCUR.2023.31},
  annote =	{Keywords: Parikh automata, History-determinism, Reversal-bounded Counter Machines}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.40
Parikh Automata over Infinite Words

Authors: Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Parikh automata extend finite automata by counters that can be tested for membership in a semilinear set, but only at the end of a run, thereby preserving many of the desirable algorithmic properties of finite automata. Here, we study the extension of the classical framework onto infinite inputs: We introduce reachability, safety, Büchi, and co-Büchi Parikh automata on infinite words and study expressiveness, closure properties, and the complexity of verification problems. We show that almost all classes of automata have pairwise incomparable expressiveness, both in the deterministic and the nondeterministic case; a result that sharply contrasts with the well-known hierarchy in the ω-regular setting. Furthermore, emptiness is shown decidable for Parikh automata with reachability or Büchi acceptance, but undecidable for safety and co-Büchi acceptance. Most importantly, we show decidability of model checking with specifications given by deterministic Parikh automata with safety or co-Büchi acceptance, but also undecidability for all other types of automata. Finally, solving games is undecidable for all types.
Cite as

Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. Parikh Automata over Infinite Words. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 40:1-40:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{guha_et_al:LIPIcs.FSTTCS.2022.40,
  author =	{Guha, Shibashis and Jecker, Isma\"{e}l and Lehtinen, Karoliina and Zimmermann, Martin},
  title =	{{Parikh Automata over Infinite Words}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{40:1--40:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.40},
  URN =		{urn:nbn:de:0030-drops-174327},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.40},
  annote =	{Keywords: Parikh automata, \omega-automata, Infinite Games}
}
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.MFCS.2021.53
A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct

Authors: Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann

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

Abstract
We study the expressiveness and succinctness of good-for-games pushdown automata (GFG-PDA) over finite words, that is, pushdown automata whose nondeterminism can be resolved based on the run constructed so far, but independently of the remainder of the input word. We prove that GFG-PDA recognise more languages than deterministic PDA (DPDA) but not all context-free languages (CFL). This class is orthogonal to unambiguous CFL. We further show that GFG-PDA can be exponentially more succinct than DPDA, while PDA can be double-exponentially more succinct than GFG-PDA. We also study GFGness in visibly pushdown automata (VPA), which enjoy better closure properties than PDA, and for which we show GFGness to be ExpTime-complete. GFG-VPA can be exponentially more succinct than deterministic VPA, while VPA can be exponentially more succinct than GFG-VPA. Both of these lower bounds are tight. Finally, we study the complexity of resolving nondeterminism in GFG-PDA. Every GFG-PDA has a positional resolver, a function that resolves nondeterminism and that is only dependant on the current configuration. Pushdown transducers are sufficient to implement the resolvers of GFG-VPA, but not those of GFG-PDA. GFG-PDA with finite-state resolvers are determinisable.
Cite as

Shibashis Guha, Ismaël Jecker, Karoliina Lehtinen, and Martin Zimmermann. A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 53:1-53:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{guha_et_al:LIPIcs.MFCS.2021.53,
  author =	{Guha, Shibashis and Jecker, Isma\"{e}l and Lehtinen, Karoliina and Zimmermann, Martin},
  title =	{{A Bit of Nondeterminism Makes Pushdown Automata Expressive and Succinct}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{53:1--53:20},
  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.53},
  URN =		{urn:nbn:de:0030-drops-144932},
  doi =		{10.4230/LIPIcs.MFCS.2021.53},
  annote =	{Keywords: Pushdown Automata, Good-for-games, Synthesis, Succintness}
}
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
DOI: 10.4230/LIPIcs.CSL.2020.29
The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas

Authors: Corto Mascle and Martin Zimmermann

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
HyperLTL, the extension of Linear Temporal Logic by trace quantifiers, is a uniform framework for expressing information flow policies by relating multiple traces of a security-critical system. HyperLTL has been successfully applied to express fundamental security policies like noninterference and observational determinism, but has also found applications beyond security, e.g., distributed protocols and coding theory. However, HyperLTL satisfiability is undecidable as soon as there are existential quantifiers in the scope of a universal one. To overcome this severe limitation to applicability, we investigate here restricted variants of the satisfiability problem to pinpoint the decidability border. First, we restrict the space of admissible models and show decidability when restricting the search space to models of bounded size or to finitely representable ones. Second, we consider formulas with restricted nesting of temporal operators and show that nesting depth one yields decidability for a slightly larger class of quantifier prefixes. We provide tight complexity bounds in almost all cases.
Cite as

Corto Mascle and Martin Zimmermann. The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{mascle_et_al:LIPIcs.CSL.2020.29,
  author =	{Mascle, Corto and Zimmermann, Martin},
  title =	{{The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel 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.CSL.2020.29},
  URN =		{urn:nbn:de:0030-drops-116720},
  doi =		{10.4230/LIPIcs.CSL.2020.29},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.34
Synthesizing Optimally Resilient Controllers

Authors: Daniel Neider, Alexander Weinert, and Martin Zimmermann

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Recently, Dallal, Neider, and Tabuada studied a generalization of the classical game-theoretic model used in program synthesis, which additionally accounts for unmodeled intermittent disturbances. In this extended framework, one is interested in computing optimally resilient strategies, i.e., strategies that are resilient against as many disturbances as possible. Dallal, Neider, and Tabuada showed how to compute such strategies for safety specifications. In this work, we compute optimally resilient strategies for a much wider range of winning conditions and show that they do not require more memory than winning strategies in the classical model. Our algorithms only have a polynomial overhead in comparison to the ones computing winning strategies. In particular, for parity conditions optimally resilient strategies are positional and can be computed in quasipolynomial time.
Cite as

Daniel Neider, Alexander Weinert, and Martin Zimmermann. Synthesizing Optimally Resilient Controllers. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 34:1-34:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{neider_et_al:LIPIcs.CSL.2018.34,
  author =	{Neider, Daniel and Weinert, Alexander and Zimmermann, Martin},
  title =	{{Synthesizing Optimally Resilient Controllers}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.34},
  URN =		{urn:nbn:de:0030-drops-97010},
  doi =		{10.4230/LIPIcs.CSL.2018.34},
  annote =	{Keywords: Controller Synthesis, Infinite Games, Resilient Strategies, Disturbances}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.36
Parity Games with Weights

Authors: Sven Schewe, Alexander Weinert, and Martin Zimmermann

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Quantitative extensions of parity games have recently attracted significant interest. These extensions include parity games with energy and payoff conditions as well as finitary parity games and their generalization to parity games with costs. Finitary parity games enjoy a special status among these extensions, as they offer a native combination of the qualitative and quantitative aspects in infinite games: the quantitative aspect of finitary parity games is a quality measure for the qualitative aspect, as it measures the limit superior of the time it takes to answer an odd color by a larger even one. Finitary parity games have been extended to parity games with costs, where each transition is labelled with a non-negative weight that reflects the costs incurred by taking it. We lift this restriction and consider parity games with costs with arbitrary integer weights. We show that solving such games is in NP cap co-NP, the signature complexity for games of this type. We also show that the protagonist has finite-state winning strategies, and provide tight exponential bounds for the memory he needs to win the game. Naturally, the antagonist may need infinite memory to win. Finally, we present tight bounds on the quality of winning strategies for the protagonist.
Cite as

Sven Schewe, Alexander Weinert, and Martin Zimmermann. Parity Games with Weights. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{schewe_et_al:LIPIcs.CSL.2018.36,
  author =	{Schewe, Sven and Weinert, Alexander and Zimmermann, Martin},
  title =	{{Parity Games with Weights}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.36},
  URN =		{urn:nbn:de:0030-drops-97037},
  doi =		{10.4230/LIPIcs.CSL.2018.36},
  annote =	{Keywords: Infinite Games, Quantitative Games, Parity Games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.10
Team Semantics for the Specification and Verification of Hyperproperties

Authors: Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We develop team semantics for Linear Temporal Logic (LTL) to express hyperproperties, which have recently been identified as a key concept in the verification of information flow properties. Conceptually, we consider an asynchronous and a synchronous variant of team semantics. We study basic properties of this new logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of these basic logics react on adding other atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL under team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties.
Cite as

Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team Semantics for the Specification and Verification of Hyperproperties. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{krebs_et_al:LIPIcs.MFCS.2018.10,
  author =	{Krebs, Andreas and Meier, Arne and Virtema, Jonni and Zimmermann, Martin},
  title =	{{Team Semantics for the Specification and Verification of Hyperproperties}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{10:1--10:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.10},
  URN =		{urn:nbn:de:0030-drops-95926},
  doi =		{10.4230/LIPIcs.MFCS.2018.10},
  annote =	{Keywords: LTL, Hyperproperties, Team Semantics, Model Checking, Satisfiability}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.57
Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems

Authors: Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We give a direct polynomial-time reduction from parity games played over the configuration graphs of collapsible pushdown systems to safety games played over the same class of graphs. That a polynomial-time reduction would exist was known since both problems are complete for the same complexity class. Coming up with a direct reduction, however, has been an open problem. Our solution to the puzzle brings together a number of techniques for pushdown games and adds three new ones. This work contributes to a recent trend of liveness to safety reductions which allow the advanced state-of-the-art in safety checking to be used for more expressive specifications.
Cite as

Matthew Hague, Roland Meyer, Sebastian Muskalla, and Martin Zimmermann. Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 57:1-57:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.MFCS.2018.57,
  author =	{Hague, Matthew and Meyer, Roland and Muskalla, Sebastian and Zimmermann, Martin},
  title =	{{Parity to Safety in Polynomial Time for Pushdown and Collapsible Pushdown Systems}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{57:1--57:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2018.57},
  URN =		{urn:nbn:de:0030-drops-96396},
  doi =		{10.4230/LIPIcs.MFCS.2018.57},
  annote =	{Keywords: Parity Games, Safety Games, Pushdown Systems, Collapsible Pushdown Systems, Higher-Order Recursion Schemes, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.30
The First-Order Logic of Hyperproperties

Authors: Bernd Finkbeiner and Martin Zimmermann

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
We investigate the logical foundations of hyperproperties. Hyperproperties generalize trace properties, which are sets of traces, to sets of sets of traces. The most prominent application of hyperproperties is information flow security: information flow policies characterize the secrecy and integrity of a system by comparing two or more execution traces, for example by comparing the observations made by an external observer on execution traces that result from different values of a secret variable. In this paper, we establish the first connection between temporal logics for hyperproperties and first-order logic. Kamp's seminal theorem (in the formulation due to Gabbay et al.) states that linear-time temporal logic (LTL) is expressively equivalent to first-order logic over the natural numbers with order. We introduce first-order logic over sets of traces and prove that HyperLTL, the extension of LTL to hyperproperties, is strictly subsumed by this logic. We furthermore exhibit a fragment that is expressively equivalent to HyperLTL, thereby establishing Kamp's theorem for hyperproperties.
Cite as

Bernd Finkbeiner and Martin Zimmermann. The First-Order Logic of Hyperproperties. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 30:1-30:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{finkbeiner_et_al:LIPIcs.STACS.2017.30,
  author =	{Finkbeiner, Bernd and Zimmermann, Martin},
  title =	{{The First-Order Logic of Hyperproperties}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{30:1--30:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.30},
  URN =		{urn:nbn:de:0030-drops-70031},
  doi =		{10.4230/LIPIcs.STACS.2017.30},
  annote =	{Keywords: Hyperproperties, Linear Temporal Logic, First-order Logic}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.28
Visibly Linear Dynamic Logic

Authors: Alexander Weinert and Martin Zimmermann

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We introduce Visibly Linear Dynamic Logic (VLDL), which extends Linear Temporal Logic (LTL) by temporal operators that are guarded by visibly pushdown languages over finite words. In VLDL one can, e.g., express that a function resets a variable to its original value after its execution, even in the presence of an unbounded number of intermediate recursive calls. We prove that VLDL describes exactly the omega-visibly pushdown languages. Thus it is strictly more expressive than LTL and able to express recursive properties of programs with unbounded call stacks. The main technical contribution of this work is a translation of VLDL into omega-visibly pushdown automata of exponential size via one-way alternating jumping automata. This translation yields exponential-time algorithms for satisfiability, validity, and model checking. We also show that visibly pushdown games with VLDL winning conditions are solvable in triply-exponential time.We prove all these problems to be complete for their respective complexity classes.
Cite as

Alexander Weinert and Martin Zimmermann. Visibly Linear Dynamic Logic. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 28:1-28:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{weinert_et_al:LIPIcs.FSTTCS.2016.28,
  author =	{Weinert, Alexander and Zimmermann, Martin},
  title =	{{Visibly Linear Dynamic Logic}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{28:1--28:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.28},
  URN =		{urn:nbn:de:0030-drops-68639},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.28},
  annote =	{Keywords: Temporal Logic, Visibly Pushdown Languages, Satisfiability, Model Checking, Infinite Games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.43
Prompt Delay

Authors: Felix Klein and Martin Zimmermann

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
Delay games are two-player games of infinite duration in which one player may delay her moves to obtain a lookahead on her opponent's moves. Recently, such games with quantitative winning conditions in weak MSO with the unbounding quantifier were studied, but their properties turned out to be unsatisfactory. In particular, unbounded lookahead is in general necessary. Here, we study delay games with winning conditions given by Prompt-LTL, Linear Temporal Logic equipped with a parameterized eventually operator whose scope is bounded. Our main result shows that solving Prompt-LTL delay games is complete for triply-exponential time. Furthermore, we give tight triply-exponential bounds on the necessary lookahead and on the scope of the parameterized eventually operator. Thus, we identify Prompt-LTL as the first known class of well-behaved quantitative winning conditions for delay games. Finally, we show that applying our techniques to delay games with omega-regular winning conditions answers open questions in the cases where the winning conditions are given by non-deterministic, universal, or alternating automata.
Cite as

Felix Klein and Martin Zimmermann. Prompt Delay. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{klein_et_al:LIPIcs.FSTTCS.2016.43,
  author =	{Klein, Felix and Zimmermann, Martin},
  title =	{{Prompt Delay}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{43:1--43:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.43},
  URN =		{urn:nbn:de:0030-drops-68786},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.43},
  annote =	{Keywords: Infinite Games, Delay Games, Prompt-LTL, LTL}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.31
Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs

Authors: Alexander Weinert and Martin Zimmermann

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
The winning condition of a parity game with costs requires an arbitrary, but fixed bound on the distance between occurrences of odd colors and the next occurrence of a larger even one. Such games quantitatively extend parity games while retaining most of their attractive properties, i.e, determining the winner is in NP and co-NP and one player has positional winning strategies. We show that the characteristics of parity games with costs are vastly different when asking for strategies realizing the minimal such bound: the solution problem becomes PSPACE-complete and exponential memory is both necessary in general and always sufficient. Thus, playing parity games with costs optimally is harder than just winning them. Moreover, we show that the tradeoff between the memory size and the realized bound is gradual in general.
Cite as

Alexander Weinert and Martin Zimmermann. Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 31:1-31:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{weinert_et_al:LIPIcs.CSL.2016.31,
  author =	{Weinert, Alexander and Zimmermann, Martin},
  title =	{{Easy to Win, Hard to Master: Optimal Strategies in Parity Games with Costs}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{31:1--31:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.31},
  URN =		{urn:nbn:de:0030-drops-65714},
  doi =		{10.4230/LIPIcs.CSL.2016.31},
  annote =	{Keywords: Parity Games with Costs, Optimal Strategies, Memory Requirements, Tradeoffs}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.519
What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead

Authors: Felix Klein and Martin Zimmermann

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
We investigate determinacy of delay games with Borel winning conditions, infinite-duration two-player games in which one player may delay her moves to obtain a lookahead on her opponent's moves. First, we prove determinacy of such games with respect to a fixed evolution of the lookahead. However, strategies in such games may depend on information about the evolution. Thus, we introduce different notions of universal strategies for both players, which are evolution-independent, and determine the exact amount of information a universal strategy needs about the history of a play and the evolution of the lookahead to be winning. In particular, we show that delay games with Borel winning conditions are determined with respect to universal strategies. Finally, we consider decidability problems, e.g., "Does a player have a universal winning strategy for delay games with a given winning condition?", for omega-regular and omega-context-free winning conditions.
Cite as

Felix Klein and Martin Zimmermann. What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 519-533, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{klein_et_al:LIPIcs.CSL.2015.519,
  author =	{Klein, Felix and Zimmermann, Martin},
  title =	{{What are Strategies in Delay Games? Borel Determinacy for Games with Lookahead}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{519--533},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.519},
  URN =		{urn:nbn:de:0030-drops-54354},
  doi =		{10.4230/LIPIcs.CSL.2015.519},
  annote =	{Keywords: Determinacy, Infinite Games, Delay Games, Borel Hierarchy}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.241
The Complexity of Counting Models of Linear-time Temporal Logic

Authors: Hazem Torfah and Martin Zimmermann

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We determine the complexity of counting models of bounded size of specifications expressed in Linear-time Temporal Logic. Counting word-models is #P-complete, if the bound is given in unary, and as hard as counting accepting runs of nondeterministic polynomial space Turing machines, if the bound is given in binary. Counting tree-models is as hard as counting accepting runs of nondeterministic exponential time Turing machines, if the bound is given in unary. For a binary encoding of the bound, the problem is at least as hard as counting accepting runs of nondeterministic exponential space Turing machines. On the other hand, it is not harder than counting accepting runs of nondeterministic doubly-exponential time Turing machines.
Cite as

Hazem Torfah and Martin Zimmermann. The Complexity of Counting Models of Linear-time Temporal Logic. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 241-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{torfah_et_al:LIPIcs.FSTTCS.2014.241,
  author =	{Torfah, Hazem and Zimmermann, Martin},
  title =	{{The Complexity of Counting Models of Linear-time Temporal Logic}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{241--252},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.241},
  URN =		{urn:nbn:de:0030-drops-48463},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.241},
  annote =	{Keywords: Model Counting, Temporal Logic, Model Checking, Counting Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.124
Cost-Parity and Cost-Streett Games

Authors: Nathanael Fijalkow and Martin Zimmermann

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

Abstract
We consider two-player games played on finite graphs equipped with costs on edges and introduce two winning conditions, cost-parity and cost-Streett, which require bounds on the cost between requests and their responses. Both conditions generalize the corresponding classical omega-regular conditions as well as the corresponding finitary conditions. For cost-parity games we show that the first player has positional winning strategies and that determining the winner lies in NP intersection Co-NP. For cost-Streett games we show that the first player has finite-state winning strategies and that determining the winner is EXPTIME-complete. This unifies the complexity results for the classical and finitary variants of these games. Both types of cost games can be solved by solving linearly many instances of their classical variants.
Cite as

Nathanael Fijalkow and Martin Zimmermann. Cost-Parity and Cost-Streett Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 124-135, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2012.124,
  author =	{Fijalkow, Nathanael and Zimmermann, Martin},
  title =	{{Cost-Parity and Cost-Streett Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{124--135},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.124},
  URN =		{urn:nbn:de:0030-drops-38538},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.124},
  annote =	{Keywords: Parity Games, Streett Games, Costs, Scoring Functions}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.264
Degrees of Lookahead in Context-free Infinite Games

Authors: Wladimir Fridman, Christof Löding, and Martin Zimmermann

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
We continue the investigation of delay games, infinite games in which one player may postpone her moves for some time to obtain a lookahead on her opponent's moves. We show that the problem of determining the winner of such a game is undecidable for deterministic context-free winning conditions. Furthermore, we show that the necessary lookahead to win a deterministic context-free delay game cannot be bounded by any elementary function. Both results hold already for restricted classes of deterministic context-free winning conditions.
Cite as

Wladimir Fridman, Christof Löding, and Martin Zimmermann. Degrees of Lookahead in Context-free Infinite Games. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 264-276, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fridman_et_al:LIPIcs.CSL.2011.264,
  author =	{Fridman, Wladimir and L\"{o}ding, Christof and Zimmermann, Martin},
  title =	{{Degrees of Lookahead in Context-free Infinite Games}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{264--276},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.264},
  URN =		{urn:nbn:de:0030-drops-32365},
  doi =		{10.4230/LIPIcs.CSL.2011.264},
  annote =	{Keywords: infinite games, delay, context-free languages}
}
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