Search Results

Documents authored by Quaas, Karin

Document
DOI: 10.4230/LIPIcs.CONCUR.2023.29
Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures

Authors: Stéphane Demri and Karin Quaas

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

Abstract
We introduce the class of tree constraint automata with data values in ℤ (equipped with the less than relation and equality predicates to constants), and we show that the nonemptiness problem is EXPTIME-complete. Using an automata-based approach, we establish that the satisfiability problem for CTL(ℤ) (CTL with constraints in ℤ) is EXPTIME-complete, and the satisfiability problem for CTL^*(ℤ) is 2ExpTime-complete (only decidability was known so far). By-product results with other concrete domains and other logics, are also briefly discussed.
Cite as

Stéphane Demri and Karin Quaas. Constraint Automata on Infinite Data Trees: from CTL(ℤ)/CTL^*(ℤ) to Decision Procedures. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{demri_et_al:LIPIcs.CONCUR.2023.29,
  author =	{Demri, St\'{e}phane and Quaas, Karin},
  title =	{{Constraint Automata on Infinite Data Trees: from CTL(\mathbb{Z})/CTL^*(\mathbb{Z}) to Decision Procedures}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{29:1--29:18},
  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.29},
  URN =		{urn:nbn:de:0030-drops-190238},
  doi =		{10.4230/LIPIcs.CONCUR.2023.29},
  annote =	{Keywords: Constraints, Constraint Automata, Temporal Logics, Infinite Data Trees}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.76
Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order

Authors: Dominik Peteler and Karin Quaas

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We study constraint automata that accept data languages on finite string values. Each transition of the automaton is labelled with a constraint restricting the string value at the current and the next position of the data word in terms of the prefix and the suffix order. We prove that the emptiness problem for such constraint automata with Büchi acceptance condition is NL-complete. We remark that since the constraints are formed by two partial orders, prefix and suffix, we cannot exploit existing techniques for similar formalisms. Our decision procedure relies on a decidable characterization for those infinite paths in the graph underlying the automaton that can be completed with string values to yield a Büchi-accepting run. Our result is - to the best of our knowledge - the first work in this context that considers both prefix and suffix, and it is a first step into answering an open question posed by Demri and Deters.
Cite as

Dominik Peteler and Karin Quaas. Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 76:1-76:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{peteler_et_al:LIPIcs.MFCS.2022.76,
  author =	{Peteler, Dominik and Quaas, Karin},
  title =	{{Deciding Emptiness for Constraint Automata on Strings with the Prefix and Suffix Order}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{76:1--76:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.76},
  URN =		{urn:nbn:de:0030-drops-168743},
  doi =		{10.4230/LIPIcs.MFCS.2022.76},
  annote =	{Keywords: Data Languages, Strings, Constraints, Prefix, Suffix, Automata, Linear Temporal Logic}
}
Document
DOI: 10.4230/DagRep.11.10.57
Unambiguity in Automata Theory (Dagstuhl Seminar 21452)

Authors: Thomas Colcombet, Karin Quaas, and Michał Skrzypczak

Published in: Dagstuhl Reports, Volume 11, Issue 10 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21452 "Unambiguity in Automata Theory". The aim of the seminar was to improve the understanding of the notion of unambiguity in automata theory, especially with respect to questions related to the expressive power, succinctness, and the tractability of unambiguous devices. The main motivation behind these studies is the hope that unambiguous machines can provide a golden balance between efficiency - sometimes not worse than for deterministic devices - and expressibility / succinctness, which often is similar to the general nondeterministic machines. These trade-offs become especially important in the models where the expressiveness or the decidability status of unambiguous machines is different from that of nondeterministic ones, as it is the case, e.g., for register automata.
Cite as

Thomas Colcombet, Karin Quaas, and Michał Skrzypczak. Unambiguity in Automata Theory (Dagstuhl Seminar 21452). In Dagstuhl Reports, Volume 11, Issue 10, pp. 57-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{colcombet_et_al:DagRep.11.10.57,
  author =	{Colcombet, Thomas and Quaas, Karin and Skrzypczak, Micha{\l}},
  title =	{{Unambiguity in Automata Theory (Dagstuhl Seminar 21452)}},
  pages =	{57--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{10},
  editor =	{Colcombet, Thomas and Quaas, Karin 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/DagRep.11.10.57},
  URN =		{urn:nbn:de:0030-drops-159282},
  doi =		{10.4230/DagRep.11.10.57},
  annote =	{Keywords: Unambiguity in Automata Theory, Dagstuhl Seminar}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.129
New Techniques for Universality in Unambiguous Register Automata

Authors: Wojciech Czerwiński, Antoine Mottet, and Karin Quaas

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
Register automata are finite automata equipped with a finite set of registers ranging over the domain of some relational structure like (ℕ; =) or (ℚ; <). Register automata process words over the domain, and along a run of the automaton, the registers can store data from the input word for later comparisons. It is long known that the universality problem, i.e., the problem to decide whether a given register automaton accepts all words over the domain, is undecidable. Recently, we proved the problem to be decidable in 2-ExpSpace if the register automaton under study is over (ℕ; =) and unambiguous, i.e., every input word has at most one accepting run; this result was shortly after improved to 2-ExpTime by Barloy and Clemente. In this paper, we go one step further and prove that the problem is in ExpSpace, and in PSpace if the number of registers is fixed. Our proof is based on new techniques that additionally allow us to show that the problem is in PSpace for single-register automata over (ℚ; <). As a third technical contribution we prove that the problem is decidable (in ExpSpace) for a more expressive model of unambiguous register automata, where the registers can take values nondeterministically, if defined over (ℕ; =) and only one register is used.
Cite as

Wojciech Czerwiński, Antoine Mottet, and Karin Quaas. New Techniques for Universality in Unambiguous Register Automata. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 129:1-129:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{czerwinski_et_al:LIPIcs.ICALP.2021.129,
  author =	{Czerwi\'{n}ski, Wojciech and Mottet, Antoine and Quaas, Karin},
  title =	{{New Techniques for Universality in Unambiguous Register Automata}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{129:1--129:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela 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.ICALP.2021.129},
  URN =		{urn:nbn:de:0030-drops-141983},
  doi =		{10.4230/LIPIcs.ICALP.2021.129},
  annote =	{Keywords: Register Automata, Data Languages, Unambiguity, Unambiguous, Universality, Containment, Language Inclusion, Equivalence}
}
Document
DOI: 10.4230/LIPIcs.STACS.2019.53
The Containment Problem for Unambiguous Register Automata

Authors: Antoine Mottet and Karin Quaas

Published in: LIPIcs, Volume 126, 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)

Abstract
We investigate the complexity of the containment problem "Does L(A)subseteq L(B) hold?", where B is an unambiguous register automaton and A is an arbitrary register automaton. We prove that the problem is decidable and give upper bounds on the computational complexity in the general case, and when B is restricted to have a fixed number of registers.
Cite as

Antoine Mottet and Karin Quaas. The Containment Problem for Unambiguous Register Automata. In 36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 126, pp. 53:1-53:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{mottet_et_al:LIPIcs.STACS.2019.53,
  author =	{Mottet, Antoine and Quaas, Karin},
  title =	{{The Containment Problem for Unambiguous Register Automata}},
  booktitle =	{36th International Symposium on Theoretical Aspects of Computer Science (STACS 2019)},
  pages =	{53:1--53:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-100-9},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{126},
  editor =	{Niedermeier, Rolf and Paul, Christophe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2019.53},
  URN =		{urn:nbn:de:0030-drops-102926},
  doi =		{10.4230/LIPIcs.STACS.2019.53},
  annote =	{Keywords: Data words, Register automata, Unambiguous Automata, Containment Problem, Language Inclusion Problem}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.33
The Complexity of Flat Freeze LTL

Authors: Benedikt Bollig, Karin Quaas, and Arnaud Sangnier

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
We consider the model-checking problem for freeze LTL on one-counter automata (OCAs). Freeze LTL extends LTL with the freeze quantifier, which allows one to store different counter values of a run in registers so that they can be compared with one another. As the model-checking problem is undecidable in general, we focus on the flat fragment of freeze LTL, in which the usage of the freeze quantifier is restricted. Recently, Lechner et al. showed that model checking for flat freeze LTL on OCAs with binary encoding of counter updates is decidable and in 2NEXPTIME. In this paper, we prove that the problem is, in fact, NEXPTIME-complete no matter whether counter updates are encoded in unary or binary. Like Lechner et al., we rely on a reduction to the reachability problem in OCAs with parameterized tests (OCAPs). The new aspect is that we simulate OCAPs by alternating two-way automata over words. This implies an exponential upper bound on the parameter values that we exploit towards an NP algorithm for reachability in OCAPs with unary updates. We obtain our main result as a corollary.
Cite as

Benedikt Bollig, Karin Quaas, and Arnaud Sangnier. The Complexity of Flat Freeze LTL. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 33:1-33:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2017.33,
  author =	{Bollig, Benedikt and Quaas, Karin and Sangnier, Arnaud},
  title =	{{The Complexity of Flat Freeze LTL}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{33:1--33:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.33},
  URN =		{urn:nbn:de:0030-drops-77993},
  doi =		{10.4230/LIPIcs.CONCUR.2017.33},
  annote =	{Keywords: one-counter automata, freeze LTL, model checking}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.15
Synchronizing Data Words for Register Automata

Authors: Parvaneh Babari, Karin Quaas, and Mahsa Shirmohammadi

Published in: LIPIcs, Volume 58, 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)

Abstract
Register automata (RAs) are finite automata extended with a finite set of registers to store and compare data. We study the concept of synchronizing data words in RAs: Does there exist a data word that sends all states of the RA to a single state? For deterministic RAs with k registers (k-DRAs), we prove that inputting data words with 2k+1 distinct data, from the infinite data domain, is sufficient to synchronize. We show that the synchronizing problem for DRAs is in general PSPACE-complete, and is NLOGSPACE-complete for 1-DRAs. For nondeterministic RAs (NRAs), we show that Ackermann(n) distinct data (where n is the size of RA) might be necessary to synchronize. The synchronizing problem for NRAs is in general undecidable, however, we establish Ackermann-completeness of the problem for 1-NRAs. Our most substantial achievement is proving NEXPTIME-completeness of the length-bounded synchronizing problem in NRAs (length encoded in binary). A variant of this last construction allows to prove that the bounded universality problem in NRAs is co-NEXPTIME-complete.
Cite as

Parvaneh Babari, Karin Quaas, and Mahsa Shirmohammadi. Synchronizing Data Words for Register Automata. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 15:1-15:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{babari_et_al:LIPIcs.MFCS.2016.15,
  author =	{Babari, Parvaneh and Quaas, Karin and Shirmohammadi, Mahsa},
  title =	{{Synchronizing Data Words for Register Automata}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{15:1--15:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-016-3},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{58},
  editor =	{Faliszewski, Piotr and Muscholl, Anca and Niedermeier, Rolf},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.15},
  URN =		{urn:nbn:de:0030-drops-64996},
  doi =		{10.4230/LIPIcs.MFCS.2016.15},
  annote =	{Keywords: data words, register automata, synchronizing problem, Ackermann-completeness, bounded universality, regular-like expressions with squaring}
}
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