11 Search Results for "Hague, Matthew"

Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2025.2
Unboundedness Problems for Formal Languages (Invited Talk)

Authors: Georg Zetzsche

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Informally, unboundedness problems are decision problems that ask about the existence of infinitely many words (satisfying certain properties) in a formal language. For example: Is a given language infinite? Or: Does a given language have super-polynomial growth? These came into focus in recent years because of their connections to downward closure computation and separability problems. Although unboundedness problems may seem difficult at first, it turns out that there are techniques that are at the same time conceptually very simple, but also apply to a surprisingly wide variety of language classes. The talk will survey recent results (and techniques) concerning unboundedness problems.
Cite as

Georg Zetzsche. Unboundedness Problems for Formal Languages (Invited Talk). In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{zetzsche:LIPIcs.FSTTCS.2025.2,
  author =	{Zetzsche, Georg},
  title =	{{Unboundedness Problems for Formal Languages}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.2},
  URN =		{urn:nbn:de:0030-drops-250810},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.2},
  annote =	{Keywords: Decidability, formal languages, unifying frameworks, downward closure, separability}
}
Document
DOI: 10.4230/LIPIcs.TIME.2025.5
Higher-Order Timed Automata and Tail Recursion

Authors: Florian Bruse

Published in: LIPIcs, Volume 355, 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)

Abstract
Timed Automata (TA) are a popular formalism to model systems in dense linear time. However, due to their finite state-space, they can only model systems with a finitary logical behavior. There are extensions to e.g., timed pushdown systems and timed recursive state machines. Higher-Order Recursion Schemes (HORS) are another popular model for infinite-state, non-regular systems, naturally stratified by their type-theoretic order. We recently introduced Real-Time Recursion schemes as an approximation of HORS to real-time systems. This paper updates Real-Time Recursion Schemes into Higher-Order Timed Automata, a formalism that defines a tree-shaped timed automaton, which is more suitable to model actual systems. We show that the model-checking problem against the timed version of the modal mu-calculus exhibits the expected complexity bounds, i.e., an increase by one exponential towards the untimed version. We also show that, in the presence of tail recursion, half an exponential can be recovered, mirroring similar gains in the untimed setting. We also give a matching lower bound for the special case of order-1 HORTA. We conjecture that this can be generalized for all orders.
Cite as

Florian Bruse. Higher-Order Timed Automata and Tail Recursion. In 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 355, pp. 5:1-5:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bruse:LIPIcs.TIME.2025.5,
  author =	{Bruse, Florian},
  title =	{{Higher-Order Timed Automata and Tail Recursion}},
  booktitle =	{32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)},
  pages =	{5:1--5:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-401-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{355},
  editor =	{Vidal, Thierry and Wa{\l}\k{e}ga, Przemys{\l}aw Andrzej},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2025.5},
  URN =		{urn:nbn:de:0030-drops-244519},
  doi =		{10.4230/LIPIcs.TIME.2025.5},
  annote =	{Keywords: Timed Automata, Higher-Order Recursion Schemes, Tree Automata, Tail Recursion}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.38
The Complexity of Separability for Semilinear Sets and Parikh Automata

Authors: Elias Rojas Collins, Chris Köcher, and Georg Zetzsche

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
In a separability problem, we are given two sets K and L from a class 𝒞, and we want to decide whether there exists a set S from a class 𝒮 such that K ⊆ S and S ∩ L = ∅. In this case, we speak of separability of sets in 𝒞 by sets in 𝒮. We study two types of separability problems. First, we consider separability of semilinear sets (i.e. subsets of ℕ^d for some d) by sets definable by quantifier-free monadic Presburger formulas (or equivalently, the recognizable subsets of ℕ^d). Here, a formula is monadic if each atom uses at most one variable. Second, we consider separability of languages of Parikh automata by regular languages. A Parikh automaton is a machine with access to counters that can only be incremented, and have to meet a semilinear constraint at the end of the run. Both of these separability problems are known to be decidable with elementary complexity. Our main results are that both problems are coNP-complete. In the case of semilinear sets, coNP-completeness holds regardless of whether the input sets are specified by existential Presburger formulas, quantifier-free formulas, or semilinear representations. Our results imply that recognizable separability of rational subsets of Σ* × ℕ^d (shown decidable by Choffrut and Grigorieff) is coNP-complete as well. Another application is that regularity of deterministic Parikh automata (where the target set is specified using a quantifier-free Presburger formula) is coNP-complete as well.
Cite as

Elias Rojas Collins, Chris Köcher, and Georg Zetzsche. The Complexity of Separability for Semilinear Sets and Parikh Automata. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 38:1-38:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{collins_et_al:LIPIcs.MFCS.2025.38,
  author =	{Collins, Elias Rojas and K\"{o}cher, Chris and Zetzsche, Georg},
  title =	{{The Complexity of Separability for Semilinear Sets and Parikh Automata}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{38:1--38:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.38},
  URN =		{urn:nbn:de:0030-drops-241457},
  doi =		{10.4230/LIPIcs.MFCS.2025.38},
  annote =	{Keywords: Vector Addition System, Separability, Regular Language}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.56
Negated String Containment Is Decidable

Authors: Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate ¬Contains(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.
Cite as

Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated String Containment Is Decidable. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 56:1-56:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.MFCS.2025.56,
  author =	{Havlena, Vojt\v{e}ch and He\v{c}ko, Michal and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej},
  title =	{{Negated String Containment Is Decidable}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{56:1--56:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56},
  URN =		{urn:nbn:de:0030-drops-241631},
  doi =		{10.4230/LIPIcs.MFCS.2025.56},
  annote =	{Keywords: not-contains, string constraints, word combinatorics, primitive word}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.142
An Efficient Quantifier Elimination Procedure for Presburger Arithmetic

Authors: Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
All known quantifier elimination procedures for Presburger arithmetic require doubly exponential time for eliminating a single block of existentially quantified variables. It has even been claimed in the literature that this upper bound is tight. We observe that this claim is incorrect and develop, as the main result of this paper, a quantifier elimination procedure eliminating a block of existentially quantified variables in singly exponential time. As corollaries, we can establish the precise complexity of numerous problems. Examples include deciding (i) monadic decomposability for existential formulas, (ii) whether an existential formula defines a well-quasi ordering or, more generally, (iii) certain formulas of Presburger arithmetic with Ramsey quantifiers. Moreover, despite the exponential blowup, our procedure shows that under mild assumptions, even NP upper bounds for decision problems about quantifier-free formulas can be transferred to existential formulas. The technical basis of our results is a kind of small model property for parametric integer programming that generalizes the seminal results by von zur Gathen and Sieveking on small integer points in convex polytopes.
Cite as

Christoph Haase, Shankara Narayanan Krishna, Khushraj Madnani, Om Swostik Mishra, and Georg Zetzsche. An Efficient Quantifier Elimination Procedure for Presburger Arithmetic. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 142:1-142:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.ICALP.2024.142,
  author =	{Haase, Christoph and Krishna, Shankara Narayanan and Madnani, Khushraj and Mishra, Om Swostik and Zetzsche, Georg},
  title =	{{An Efficient Quantifier Elimination Procedure for Presburger Arithmetic}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{142:1--142:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.142},
  URN =		{urn:nbn:de:0030-drops-202856},
  doi =		{10.4230/LIPIcs.ICALP.2024.142},
  annote =	{Keywords: Presburger arithmetic, quantifier elimination, parametric integer programming, convex geometry}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.42
Optimal Strategies in Pushdown Reachability Games

Authors: Arnaud Carayol and Matthew Hague

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

Abstract
An algorithm for computing optimal strategies in pushdown reachability games was given by Cachat. We show that the information tracked by this algorithm is too coarse and the strategies constructed are not necessarily optimal. We then show that the algorithm can be refined to recover optimality. Through a further non-trivial argument the refined algorithm can be run in 2EXPTIME by bounding the play-lengths tracked to those that are at most doubly exponential. This is optimal in the sense that there exists a game for which the optimal strategy requires a doubly exponential number of moves to reach a target configuration.
Cite as

Arnaud Carayol and Matthew Hague. Optimal Strategies in Pushdown Reachability Games. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 42:1-42:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.MFCS.2018.42,
  author =	{Carayol, Arnaud and Hague, Matthew},
  title =	{{Optimal Strategies in Pushdown Reachability Games}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{42:1--42:14},
  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.42},
  URN =		{urn:nbn:de:0030-drops-96248},
  doi =		{10.4230/LIPIcs.MFCS.2018.42},
  annote =	{Keywords: Pushdown Systems, Reachability Games, Optimal Strategies, Formal Methods, Context Free}
}
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.MFCS.2017.59
Domains for Higher-Order Games

Authors: Matthew Hague, Roland Meyer, and Sebastian Muskalla

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
We study two-player inclusion games played over word-generating higher-order recursion schemes. While inclusion checks are known to capture verification problems, two-player games generalize this relationship to program synthesis. In such games, non-terminals of the grammar are controlled by opposing players. The goal of the existential player is to avoid producing a word that lies outside of a regular language of safe words. We contribute a new domain that provides a representation of the winning region of such games. Our domain is based on (functions over) potentially infinite Boolean formulas with words as atomic propositions. We develop an abstract interpretation framework that we instantiate to abstract this domain into a domain where the propositions are replaced by states of a finite automaton. This second domain is therefore finite and we obtain, via standard fixed-point techniques, a direct algorithm for the analysis of two-player inclusion games. We show, via a second instantiation of the framework, that our finite domain can be optimized, leading to a (k+1)EXP algorithm for order-k recursion schemes. We give a matching lower bound, showing that our approach is optimal. Since our approach is based on standard Kleene iteration, existing techniques and tools for fixed-point computations can be applied.
Cite as

Matthew Hague, Roland Meyer, and Sebastian Muskalla. Domains for Higher-Order Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 59:1-59:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.MFCS.2017.59,
  author =	{Hague, Matthew and Meyer, Roland and Muskalla, Sebastian},
  title =	{{Domains for Higher-Order Games}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{59:1--59:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.59},
  URN =		{urn:nbn:de:0030-drops-81409},
  doi =		{10.4230/LIPIcs.MFCS.2017.59},
  annote =	{Keywords: higher-order recursion schemes, games, semantics, abstract interpretation, fixed points}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.313
Saturation of Concurrent Collapsible Pushdown Systems

Authors: Matthew Hague

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

Abstract
Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multi-stack collapsible pushdown systems have been little studied. Here, we study ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques, showing decidability of control state reachability and giving a regular representation of all configurations that can reach a given control state.
Cite as

Matthew Hague. Saturation of Concurrent Collapsible Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 313-325, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{hague:LIPIcs.FSTTCS.2013.313,
  author =	{Hague, Matthew},
  title =	{{Saturation of Concurrent Collapsible Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{313--325},
  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.313},
  URN =		{urn:nbn:de:0030-drops-43829},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.313},
  annote =	{Keywords: Concurrency, Automata, Higher-Order, Verification, Model-Checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.457
Parameterised Pushdown Systems with Non-Atomic Writes

Authors: Matthew Hague

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

Abstract
We consider the master/slave parameterised reachability problem for networks of pushdown systems, where communication is via a global store using only non-atomic reads and writes. We show that the control-state reachability problem is decidable. As part of the result, we provide a constructive extension of a theorem by Ehrenfeucht and Rozenberg to produce an NFA equivalent to certain kinds of CFG. Finally, we show that the non-parameterised version is undecidable.
Cite as

Matthew Hague. Parameterised Pushdown Systems with Non-Atomic Writes. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 457-468, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{hague:LIPIcs.FSTTCS.2011.457,
  author =	{Hague, Matthew},
  title =	{{Parameterised Pushdown Systems with Non-Atomic Writes}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{457--468},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-34-7},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{13},
  editor =	{Chakraborty, Supratik and Kumar, Amit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2011.457},
  URN =		{urn:nbn:de:0030-drops-33485},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.457},
  annote =	{Keywords: Verification, Concurrency, Pushdown Systems, Reachability, Parameterised Systems, Non-atomicity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.228
The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems

Authors: Matthew Hague and Anthony Widjaja To

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

Abstract
We study (collapsible) higher-order pushdown systems --- theoretically robust and well-studied models of higher-order programs --- along with their natural subclass called (collapsible) higher-order basic process algebras. We provide a comprehensive analysis of the model checking complexity of a range of both branching-time and linear-time temporal logics. We obtain tight bounds on data, expression, and combined-complexity for both (collapsible) higher-order pushdown systems and (collapsible) higher-order basic process algebra. At order-$k$, results range from polynomial to $(k+1)$-exponential time. Finally, we study (collapsible) higher-order basic process algebras as graph generators and show that they are almost as powerful as (collapsible) higher-order pushdown systems up to MSO interpretations.
Cite as

Matthew Hague and Anthony Widjaja To. The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 228-239, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{hague_et_al:LIPIcs.FSTTCS.2010.228,
  author =	{Hague, Matthew and To, Anthony Widjaja},
  title =	{{The Complexity of Model Checking (Collapsible) Higher-Order Pushdown Systems}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{228--239},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.228},
  URN =		{urn:nbn:de:0030-drops-28663},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.228},
  annote =	{Keywords: Higher-Order, Collapsible, Pushdown Systems, Temporal Logics, Complexity, Model Checking}
}
  • Refine by Type
  • 11 Document/PDF
  • 4 Document/HTML

  • Refine by Publication Year
  • 4 2025
  • 1 2024
  • 2 2018
  • 1 2017
  • 1 2013
  • Show More...

  • Refine by Author
  • 6 Hague, Matthew
  • 3 Zetzsche, Georg
  • 2 Meyer, Roland
  • 2 Muskalla, Sebastian
  • 1 Bruse, Florian
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs

  • Refine by Classification
  • 2 Theory of computation → Automata over infinite objects
  • 2 Theory of computation → Logic and verification
  • 2 Theory of computation → Models of computation
  • 2 Theory of computation → Regular languages
  • 1 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 4 Pushdown Systems
  • 2 Concurrency
  • 2 Higher-Order
  • 2 Higher-Order Recursion Schemes
  • 2 Model Checking
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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