Search Results

Documents authored by Piórkowski, Radosław

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.13
Universal Quantification Makes Automatic Structures Hard to Decide

Authors: Christoph Haase and Radosław Piórkowski

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

Abstract
Automatic structures are structures whose universe and relations can be represented as regular languages. It follows from the standard closure properties of regular languages that the first-order theory of an automatic structure is decidable. While existential quantifiers can be eliminated in linear time by application of a homomorphism, universal quantifiers are commonly eliminated via the identity ∀x.Φ≡¬(∃x.¬Φ). If Φ is represented in the standard way as an NFA, a priori this approach results in a doubly exponential blow-up. However, the recent literature has shown that there are classes of automatic structures for which universal quantifiers can be eliminated by different means without this blow-up by treating them as first-class citizens and not resorting to double complementation. While existing lower bounds for some classes of automatic structures show that a singly exponential blow-up is unavoidable when eliminating a universal quantifier, it is not known whether there may be better approaches that avoid the naïve doubly exponential blow-up, perhaps at least in restricted settings. In this paper, we answer this question negatively and show that there is a family of NFA representing automatic relations for which the minimal NFA recognising the language after eliminating a single universal quantifier is doubly exponential, and deciding whether this language is empty is ExpSpace-complete.
Cite as

Christoph Haase and Radosław Piórkowski. Universal Quantification Makes Automatic Structures Hard to Decide. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{haase_et_al:LIPIcs.CONCUR.2023.13,
  author =	{Haase, Christoph and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Universal Quantification Makes Automatic Structures Hard to Decide}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{13:1--13:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.13},
  URN =		{urn:nbn:de:0030-drops-190075},
  doi =		{10.4230/LIPIcs.CONCUR.2023.13},
  annote =	{Keywords: automatic structures, universal projection, state complexity, tiling problems}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2020.42
Determinisability of One-Clock Timed Automata

Authors: Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski

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

Abstract
The deterministic membership problem for timed automata asks whether the timed language recognised by a nondeterministic timed automaton can be recognised by a deterministic timed automaton. We show that the problem is decidable when the input automaton is a one-clock nondeterministic timed automaton without epsilon transitions and the number of clocks of the deterministic timed automaton is fixed. We show that the problem in all the other cases is undecidable, i.e., when either 1) the input nondeterministic timed automaton has two clocks or more, or 2) it uses epsilon transitions, or 3) the number of clocks of the output deterministic automaton is not fixed.
Cite as

Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Determinisability of One-Clock Timed Automata. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.CONCUR.2020.42,
  author =	{Clemente, Lorenzo and Lasota, S{\l}awomir and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Determinisability of One-Clock Timed Automata}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.42},
  URN =		{urn:nbn:de:0030-drops-128542},
  doi =		{10.4230/LIPIcs.CONCUR.2020.42},
  annote =	{Keywords: Timed automata, determinisation, deterministic membership problem}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2020.121
Timed Games and Deterministic Separability

Authors: Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski

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

Abstract
We study a generalisation of Büchi-Landweber games to the timed setting. The winning condition is specified by a non-deterministic timed automaton with epsilon transitions and only Player I can elapse time. We show that for fixed number of clocks and maximal numerical constant available to Player II, it is decidable whether she has a winning timed controller using these resources. More interestingly, we also show that the problem remains decidable even when the maximal numerical constant is not specified in advance, which is an important technical novelty not present in previous literature on timed games. We complement these two decidability result by showing undecidability when the number of clocks available to Player II is not fixed. As an application of timed games, and our main motivation to study them, we show that they can be used to solve the deterministic separability problem for nondeterministic timed automata with epsilon transitions. This is a novel decision problem about timed automata which has not been studied before. We show that separability is decidable when the number of clocks of the separating automaton is fixed and the maximal constant is not. The problem whether separability is decidable without bounding the number of clocks of the separator remains an interesting open problem.
Cite as

Lorenzo Clemente, Sławomir Lasota, and Radosław Piórkowski. Timed Games and Deterministic Separability. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 168, pp. 121:1-121:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{clemente_et_al:LIPIcs.ICALP.2020.121,
  author =	{Clemente, Lorenzo and Lasota, S{\l}awomir and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{Timed Games and Deterministic Separability}},
  booktitle =	{47th International Colloquium on Automata, Languages, and Programming (ICALP 2020)},
  pages =	{121:1--121:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-138-2},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{168},
  editor =	{Czumaj, Artur and Dawar, Anuj and Merelli, Emanuela},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.121},
  URN =		{urn:nbn:de:0030-drops-125282},
  doi =		{10.4230/LIPIcs.ICALP.2020.121},
  annote =	{Keywords: Timed automata, separability problems, timed games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2019.62
New Pumping Technique for 2-Dimensional VASS

Authors: Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski

Published in: LIPIcs, Volume 138, 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)

Abstract
We propose a new pumping technique for 2-dimensional vector addition systems with states (2-VASS) building on natural geometric properties of runs. We illustrate its applicability by reproving an exponential bound on the length of the shortest accepting run, and by proving a new pumping lemma for languages of 2-VASS. The technique is expected to be useful for settling questions concerning languages of 2-VASS, e.g., for establishing decidability status of the regular separability problem.
Cite as

Wojciech Czerwiński, Sławomir Lasota, Christof Löding, and Radosław Piórkowski. New Pumping Technique for 2-Dimensional VASS. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 62:1-62:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.MFCS.2019.62,
  author =	{Czerwi\'{n}ski, Wojciech and Lasota, S{\l}awomir and L\"{o}ding, Christof and Pi\'{o}rkowski, Rados{\l}aw},
  title =	{{New Pumping Technique for 2-Dimensional VASS}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{62:1--62:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-117-7},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{138},
  editor =	{Rossmanith, Peter and Heggernes, Pinar and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.62},
  URN =		{urn:nbn:de:0030-drops-110066},
  doi =		{10.4230/LIPIcs.MFCS.2019.62},
  annote =	{Keywords: vector addition systems with states, pumping, decidability}
}
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 About DROPS Imprint Privacy Contact