3 Search Results for "Hazard, Emile"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.12
Explorability in Pushdown Automata

Authors: Ayaan Bedi and Karoliina Lehtinen

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

Abstract
We study explorability, a measure of nondeterminism in pushdown automata, which generalises history-determinism. An automaton is k-explorable if, while reading the input, it suffices to follow k concurrent runs, built step-by-step based only on the input seen so far, to construct an accepting one, if it exists. We show that the class of explorable PDAs lies strictly between history-deterministic and fully nondeterministic PDAs in terms of both expressiveness and succinctness. In fact increasing explorability induces an infinite hierarchy: each level k defines a strictly more expressive class than level k-1, yet the entire class remains less expressive than general nondeterministic PDAs. We then introduce a parameterized notion of explorability, where the number of runs may depend on input length, and show that exponential explorability precisely captures the context-free languages. Finally, we prove that explorable PDAs can be doubly exponentially more succinct than history-deterministic ones, and that the succinctness gap between deterministic and 2-explorable PDAs is not recursively enumerable. These results position explorability as a robust and operationally meaningful measure of nondeterminism for pushdown systems.
Cite as

Ayaan Bedi and Karoliina Lehtinen. Explorability in Pushdown Automata. 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. 12:1-12:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bedi_et_al:LIPIcs.FSTTCS.2025.12,
  author =	{Bedi, Ayaan and Lehtinen, Karoliina},
  title =	{{Explorability in Pushdown Automata}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{12:1--12:18},
  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.12},
  URN =		{urn:nbn:de:0030-drops-250921},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.12},
  annote =	{Keywords: Pushdown automata, nondeterminism, explorability, history-determinism}
}
Document
DOI: 10.4230/LIPIcs.CSL.2023.24
Explorable Automata

Authors: Emile Hazard and Denis Kuperberg

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one. We show that recognizing HD parity automata of fixed index among explorable ones is in PTime, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is ExpTime-complete, in the case of finite words or Büchi automata. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show that all reachability automata are ω-explorable, but this is not the case for safety ones. We finally show ExpTime-completeness for ω-explorability of automata on infinite words for the safety and co-Büchi acceptance conditions.
Cite as

Emile Hazard and Denis Kuperberg. Explorable Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 24:1-24:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{hazard_et_al:LIPIcs.CSL.2023.24,
  author =	{Hazard, Emile and Kuperberg, Denis},
  title =	{{Explorable Automata}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{24:1--24:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.24},
  URN =		{urn:nbn:de:0030-drops-174852},
  doi =		{10.4230/LIPIcs.CSL.2023.24},
  annote =	{Keywords: Nondeterminism, automata, complexity}
}
Document
DOI: 10.4230/LIPIcs.CSL.2022.23
Cyclic Proofs for Transfinite Expressions

Authors: Emile Hazard and Denis Kuperberg

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract
We introduce a cyclic proof system for proving inclusions of transfinite expressions, describing languages of words of ordinal length. We show that recognising valid cyclic proofs is decidable, that our system is sound and complete, and well-behaved with respect to cuts. Moreover, cyclic proofs can be effectively computed from expressions inclusions. We show how to use this to obtain a Pspace algorithm for transfinite expression inclusion.
Cite as

Emile Hazard and Denis Kuperberg. Cyclic Proofs for Transfinite Expressions. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{hazard_et_al:LIPIcs.CSL.2022.23,
  author =	{Hazard, Emile and Kuperberg, Denis},
  title =	{{Cyclic Proofs for Transfinite Expressions}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.23},
  URN =		{urn:nbn:de:0030-drops-157433},
  doi =		{10.4230/LIPIcs.CSL.2022.23},
  annote =	{Keywords: transfinite expressions, transfinite automata, cyclic proofs}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2023
  • 1 2022

  • Refine by Author
  • 2 Hazard, Emile
  • 2 Kuperberg, Denis
  • 1 Bedi, Ayaan
  • 1 Lehtinen, Karoliina

  • Refine by Series/Journal
  • 3 LIPIcs

  • Refine by Classification
  • 1 Theory of computation → Automata extensions
  • 1 Theory of computation → Automata over infinite objects
  • 1 Theory of computation → Formal languages and automata theory
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Proof theory

  • Refine by Keyword
  • 1 Nondeterminism
  • 1 Pushdown automata
  • 1 automata
  • 1 complexity
  • 1 cyclic proofs
  • 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