Search Results

Documents authored by Göller, Stefan

Document
DOI: 10.4230/LIPIcs.STACS.2024.38
The AC⁰-Complexity of Visibly Pushdown Languages

Authors: Stefan Göller and Nathan Grosshans

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
We study the question of which visibly pushdown languages (VPLs) are in the complexity class AC⁰ and how to effectively decide this question. Our contribution is to introduce a particular subclass of one-turn VPLs, called intermediate VPLs, for which the raised question is entirely unclear: to the best of our knowledge our research community is unaware of containment or non-containment in AC⁰ for any language in our newly introduced class. Our main result states that there is an algorithm that, given a visibly pushdown automaton, correctly outputs exactly one of the following: that its language L is in AC⁰, some m ≥ 2 such that MODₘ (the words over {0,1} having a number of 1’s divisible by m) is constant-depth reducible to L (implying that L is not in AC⁰), or a finite disjoint union of intermediate VPLs that L is constant-depth equivalent to. In the latter of the three cases one can moreover effectively compute k,l ∈ ℕ_{> 0} with k≠l such that the concrete intermediate VPL L(S → ε ∣ ac^{k-1}Sb₁ ∣ ac^{l-1}Sb₂) is constant-depth reducible to the language L. Due to their particular nature we conjecture that either all intermediate VPLs are in AC⁰ or all are not. As a corollary of our main result we obtain that in case the input language is a visibly counter language our algorithm can effectively determine if it is in AC⁰ - hence our main result generalizes a result by Krebs et al. stating that it is decidable if a given visibly counter language is in AC⁰ (when restricted to well-matched words). For our proofs we revisit so-called Ext-algebras (introduced by Czarnetzki et al.), which are closely related to forest algebras (introduced by Bojańczyk and Walukiewicz), and use Green’s relations.
Cite as

Stefan Göller and Nathan Grosshans. The AC⁰-Complexity of Visibly Pushdown Languages. In 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2024.38,
  author =	{G\"{o}ller, Stefan and Grosshans, Nathan},
  title =	{{The AC⁰-Complexity of Visibly Pushdown Languages}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.38},
  URN =		{urn:nbn:de:0030-drops-197483},
  doi =		{10.4230/LIPIcs.STACS.2024.38},
  annote =	{Keywords: Visibly pushdown languages, Circuit Complexity, AC0}
}
Document
DOI: 10.4230/LIPIcs.STACS.2021.36
Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete

Authors: Stefan Göller and Mathieu Hilaire

Published in: LIPIcs, Volume 187, 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)

Abstract
Parametric timed automata (PTA) have been introduced by Alur, Henzinger, and Vardi as an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACE^NEXP. Our main result is that the reachability problem for parametric timed automata over two parametric clocks and one parameter is EXPSPACE-complete. For the EXPSPACE lower bound we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (in turn based on Barrington’s Theorem) and a logspace translation of numbers in Chinese Remainder Representation to binary representation due to Chiu, Davida, and Litow. It is shown that with small PTA over two parametric clocks and one parameter one can simulate serializability computations. For the EXPSPACE upper bound, we first give a careful exponential time reduction from PTA over two parametric clocks and one parameter to a (slight subclass of) parametric one-counter automata over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. For solving the reachability problem for parametric one-counter automata with one parameter, we provide a series of techniques to partition a fictitious run into several carefully chosen subruns that allow us to prove that it is sufficient to consider a parameter value of exponential magnitude only. This allows us to show a doubly-exponential upper bound on the value of the only parameter of a PTA over two parametric clocks and one parameter. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters) and, if decidability holds, determining its precise computational complexity.
Cite as

Stefan Göller and Mathieu Hilaire. Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete. In 38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 187, pp. 36:1-36:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2021.36,
  author =	{G\"{o}ller, Stefan and Hilaire, Mathieu},
  title =	{{Reachability in Two-Parametric Timed Automata with One Parameter Is EXPSPACE-Complete}},
  booktitle =	{38th International Symposium on Theoretical Aspects of Computer Science (STACS 2021)},
  pages =	{36:1--36:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-180-1},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{187},
  editor =	{Bl\"{a}ser, Markus and Monmege, Benjamin},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2021.36},
  URN =		{urn:nbn:de:0030-drops-136817},
  doi =		{10.4230/LIPIcs.STACS.2021.36},
  annote =	{Keywords: Parametric Timed Automata, Computational Complexity, Reachability}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.14
On Büchi One-Counter Automata

Authors: Stanislav Böhm, Stefan Göller, Simon Halfon, and Piotr Hofman

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

Abstract
Equivalence of deterministic pushdown automata is a famous problem in theoretical computer science whose decidability has been shown by Sénizergues. Our first result shows that decidability no longer holds when moving from finite words to infinite words. This solves an open problem that has recently been raised by Löding. In fact, we show that already the equivalence problem for deterministic Büchi one-counter automata is undecidable. Hence, the decidability border is rather tight when taking into account a recent result by Löding and Repke that equivalence of deterministic weak parity pushdown automata (a subclass of deterministic Büchi pushdown automata) is decidable. Another known result on finite words is that the universality problem for vector addition systems is decidable. We show undecidability when moving to infinite words. In fact, we prove that already the universality problem for nondeterministic Büchi one-counter nets (or equivalently vector addition systems with one unbounded dimension) is undecidable.
Cite as

Stanislav Böhm, Stefan Göller, Simon Halfon, and Piotr Hofman. On Büchi One-Counter Automata. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bohm_et_al:LIPIcs.STACS.2017.14,
  author =	{B\"{o}hm, Stanislav and G\"{o}ller, Stefan and Halfon, Simon and Hofman, Piotr},
  title =	{{On B\"{u}chi One-Counter Automata}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{14:1--14:13},
  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.14},
  URN =		{urn:nbn:de:0030-drops-70194},
  doi =		{10.4230/LIPIcs.STACS.2017.14},
  annote =	{Keywords: infinite words, deterministic pushdown automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.19
On Long Words Avoiding Zimin Patterns

Authors: Arnaud Carayol and Stefan Göller

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

Abstract
A pattern is encountered in a word if some infix of the word is the image of the pattern under some non-erasing morphism. A pattern p is unavoidable if, over every finite alphabet, every sufficiently long word encounters p. A theorem by Zimin and independently by Bean, Ehrenfeucht and McNulty states that a pattern over n distinct variables is unavoidable if, and only if, p itself is encountered in the n-th Zimin pattern. Given an alphabet size k, we study the minimal length f(n,k) such that every word of length f(n,k) encounters the n-th Zimin pattern. It is known that f is upper-bounded by a tower of exponentials. Our main result states that f(n,k) is lower-bounded by a tower of n-3 exponentials, even for k=2. To the best of our knowledge, this improves upon a previously best-known doubly-exponential lower bound. As a further result, we prove a doubly-exponential upper bound for encountering Zimin patterns in the abelian sense.
Cite as

Arnaud Carayol and Stefan Göller. On Long Words Avoiding Zimin Patterns. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 19:1-19:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{carayol_et_al:LIPIcs.STACS.2017.19,
  author =	{Carayol, Arnaud and G\"{o}ller, Stefan},
  title =	{{On Long Words Avoiding Zimin Patterns}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{19:1--19:13},
  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.19},
  URN =		{urn:nbn:de:0030-drops-70140},
  doi =		{10.4230/LIPIcs.STACS.2017.19},
  annote =	{Keywords: Unavoidable patterns, combinatorics on words, lower bounds}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.12
On the Parallel Complexity of Bisimulation on Finite Systems

Authors: Moses Ganardi, Stefan Göller, and Markus Lohrey

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

Abstract
In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC^1, respectively. This solves an open problem from Balcázar, Gabarró, and Sántha. We also show that the simulation problem is P-complete even for graphs of bounded path-width.
Cite as

Moses Ganardi, Stefan Göller, and Markus Lohrey. On the Parallel Complexity of Bisimulation on Finite Systems. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{ganardi_et_al:LIPIcs.CSL.2016.12,
  author =	{Ganardi, Moses and G\"{o}ller, Stefan and Lohrey, Markus},
  title =	{{On the Parallel Complexity of Bisimulation on Finite Systems}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{12:1--12: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.12},
  URN =		{urn:nbn:de:0030-drops-65522},
  doi =		{10.4230/LIPIcs.CSL.2016.12},
  annote =	{Keywords: bisimulation, computational complexity, tree width}
}
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.CSL.2013.332
The Fixed-Parameter Tractability of Model Checking Concurrent Systems

Authors: Stefan Göller

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
We study the fixed-parameter complexity of model checking temporal logics on concurrent systems that are modeled as the product of finite systems and where the size of the formula is the parameter. We distinguish between asynchronous product and synchronous product. Sometimes it is possible to show that there is an algorithm for this with running time (\sum_i T_i|)O(1) * f(|\phi|), where the T_i are the component systems and \phi is the formula and f is computable function, thus model checking is fixed-parameter tractable when the size of the formula is the parameter. In this paper we concern ourselves with the question, provided fixed-parameter tractability is known, whether it holds for an elementary function f. Negative answers to this question are provided for modal logic and EF logic: Depending on the mode of synchronization we show the non-existence of such an elementary function f under different assumptions from (parameterized) complexity theory.
Cite as

Stefan Göller. The Fixed-Parameter Tractability of Model Checking Concurrent Systems. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 332-347, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{goller:LIPIcs.CSL.2013.332,
  author =	{G\"{o}ller, Stefan},
  title =	{{The Fixed-Parameter Tractability of Model Checking Concurrent Systems}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{332--347},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.332},
  URN =		{urn:nbn:de:0030-drops-42062},
  doi =		{10.4230/LIPIcs.CSL.2013.332},
  annote =	{Keywords: Model Checking, Concurrent Systems, Parameterized Complexity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.160
On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two

Authors: Christopher Broadbent and Stefan Göller

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

Abstract
We show that bisimulation equivalence of order-two pushdown automata is undecidable. Moreover, we study the lower order problem of higher-order pushdown automata, which asks, given an order-k pushdown automaton and some k'<k, to determine if there exists a reachable configuration that is bisimilar to some order-k' pushdown automaton. We show that the lower order problem is undecidable for each k >= 2 even when the input k-PDA is deterministic and real-time.
Cite as

Christopher Broadbent and Stefan Göller. On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 160-172, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{broadbent_et_al:LIPIcs.FSTTCS.2012.160,
  author =	{Broadbent, Christopher and G\"{o}ller, Stefan},
  title =	{{On Bisimilarity of Higher-Order Pushdown Automata: Undecidability at Order Two}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{160--172},
  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.160},
  URN =		{urn:nbn:de:0030-drops-38583},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.160},
  annote =	{Keywords: Bisimulation equivalence, Higher-order pushdown automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2012.148
Concurrency Makes Simple Theories Hard

Authors: Stefan Göller and Anthony Widjaja Lin

Published in: LIPIcs, Volume 14, 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)

Abstract
A standard way of building concurrent systems is by composing several individual processes by product operators. We show that even the simplest notion of product operators (i.e. asynchronous products) suffices to increase the complexity of model checking simple logics like Hennessy-Milner (HM) logic and its extension with the reachability operator (EF-logic) from PSPACE to nonelementary. In particular, this nonelementary jump happens for EF-logic when we consider individual processes represented by pushdown systems (indeed, even with only one control state). Using this result, we prove nonelementary lower bounds on the size of formula decompositions provided by Feferman-Vaught (de)compositional methods for HM and EF logics, which reduce theories of asynchronous products to theories of the components. Finally, we show that the same nonelementary lower bounds also hold when we consider the relativization of such compositional methods to finite systems.
Cite as

Stefan Göller and Anthony Widjaja Lin. Concurrency Makes Simple Theories Hard. In 29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 14, pp. 148-159, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2012.148,
  author =	{G\"{o}ller, Stefan and Widjaja Lin, Anthony},
  title =	{{Concurrency Makes Simple Theories Hard}},
  booktitle =	{29th International Symposium on Theoretical Aspects of Computer Science (STACS 2012)},
  pages =	{148--159},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-35-4},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{14},
  editor =	{D\"{u}rr, Christoph and Wilke, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2012.148},
  URN =		{urn:nbn:de:0030-drops-34214},
  doi =		{10.4230/LIPIcs.STACS.2012.148},
  annote =	{Keywords: Modal Logic, Model Checking, Asynchronous Product, Pushdown Systems, Feferman-Vaught, Nonelementary lower bounds}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2011.276
The First-Order Theory of Ground Tree Rewrite Graphs

Authors: Stefan Göller and Markus Lohrey

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

Abstract
We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(2^{2^{poly(n)}},O(n). Providing a matching lower bound, we show that there is some fixed ground tree rewrite graph whose first-order theory is hard for ATIME(2^{2^{poly(n)}},poly(n)) with respect to logspace reductions. Finally, we prove that there exists a fixed ground tree rewrite graph together with a single unary predicate in form of a regular tree language such that the resulting structure has a non-elementary first-order theory.
Cite as

Stefan Göller and Markus Lohrey. The First-Order Theory of Ground Tree Rewrite Graphs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 13, pp. 276-287, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.FSTTCS.2011.276,
  author =	{G\"{o}ller, Stefan and Lohrey, Markus},
  title =	{{The First-Order Theory of Ground Tree Rewrite Graphs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011)},
  pages =	{276--287},
  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.276},
  URN =		{urn:nbn:de:0030-drops-33220},
  doi =		{10.4230/LIPIcs.FSTTCS.2011.276},
  annote =	{Keywords: ground tree rewriting systems, first-order theories, complexity}
}
Document
DOI: 10.4230/LIPIcs.STACS.2010.2472
Branching-time Model Checking of One-counter Processes

Authors: Stefan Göller and Markus Lohrey

Published in: LIPIcs, Volume 5, 27th International Symposium on Theoretical Aspects of Computer Science (2010)

Abstract
One-counter processes (OCPs) are pushdown processes which operate only on a unary stack alphabet. We study the computational complexity of model checking computation tree logic ($\CTL$) over OCPs. A $\PSPACE$ upper bound is inherited from the modal $\mu$-calculus for this problem. First, we analyze the periodic behaviour of $\CTL$ over OCPs and derive a model checking algorithm whose running time is exponential only in the number of control locations and a syntactic notion of the formula that we call leftward until depth. Thus, model checking fixed OCPs against $\CTL$ formulas with a fixed leftward until depth is in $\P$. This generalizes a result of the first author, Mayr, and To for the expression complexity of $\CTL$'s fragment $\EF$. Second, we prove that already over some fixed OCP, $\CTL$ model checking is $\PSPACE$-hard. Third, we show that there already exists a fixed $\CTL$ formula for which model checking of OCPs is $\PSPACE$-hard. For the latter, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform $\NC^1$ and (ii) $\PSPACE$ is $\AC^0$-serializable. We demonstrate that our approach can be used to answer further open questions.
Cite as

Stefan Göller and Markus Lohrey. Branching-time Model Checking of One-counter Processes. In 27th International Symposium on Theoretical Aspects of Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 5, pp. 405-416, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:LIPIcs.STACS.2010.2472,
  author =	{G\"{o}ller, Stefan and Lohrey, Markus},
  title =	{{Branching-time Model Checking of One-counter Processes}},
  booktitle =	{27th International Symposium on Theoretical Aspects of Computer Science},
  pages =	{405--416},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-16-3},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{5},
  editor =	{Marion, Jean-Yves and Schwentick, Thomas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2010.2472},
  URN =		{urn:nbn:de:0030-drops-24722},
  doi =		{10.4230/LIPIcs.STACS.2010.2472},
  annote =	{Keywords: Model checking, computation tree logic, complexity theory}
}
Document
DOI: 10.4230/DagSemProc.07441.5
PDL with Intersection and Converse is 2EXP-complete

Authors: Stefan Göller, Markus Lohrey, and Carsten Lutz

Published in: Dagstuhl Seminar Proceedings, Volume 7441, Algorithmic-Logical Theory of Infinite Structures (2008)

Abstract
The logic ICPDL is the expressive extension of Propositional Dynamic Logic (PDL), which admits intersection and converse as program operators. The result of this paper is containment of ICPDL-satisfiability in $2$EXP, which improves the previously known non-elementary upper bound and implies $2$EXP-completeness due to an existing lower bound for PDL with intersection (IPDL). The proof proceeds showing that every satisfiable ICPDL formula has model of tree width at most two. Next, we reduce satisfiability in ICPDL to $omega$-regular tree satisfiability in ICPDL. In the latter problem the set of possible models is restricted to trees of an $omega$-regular tree language. In the final step,$omega$-regular tree satisfiability is reduced the emptiness problem for alternating two-way automata on infinite trees. In this way, a more elegant proof is obtained for Danecki's difficult result that satisfiability in IPDL is in $2EXP$.
Cite as

Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with Intersection and Converse is 2EXP-complete. In Algorithmic-Logical Theory of Infinite Structures. Dagstuhl Seminar Proceedings, Volume 7441, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{goller_et_al:DagSemProc.07441.5,
  author =	{G\"{o}ller, Stefan and Lohrey, Markus and Lutz, Carsten},
  title =	{{PDL with Intersection and Converse is 2EXP-complete}},
  booktitle =	{Algorithmic-Logical Theory of Infinite Structures},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7441},
  editor =	{Rod Downey and Bakhadyr Khoussainov and Dietrich Kuske and Markus Lohrey and Moshe Y. Vardi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07441.5},
  URN =		{urn:nbn:de:0030-drops-14093},
  doi =		{10.4230/DagSemProc.07441.5},
  annote =	{Keywords: Satisfiability, Propositional Dynamic Logic, Computational 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