4 Search Results for "Bose, Sougata"


Document
History-Deterministic Vector Addition Systems

Authors: Sougata Bose, David Purser, and Patrick Totzke

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


Abstract
We consider history-determinism, a restricted form of non-determinism, for Vector Addition Systems with States (VASS) when used as acceptors to recognise languages of finite words. History-determinism requires that the non-deterministic choices can be resolved on-the-fly; based on the past and without jeopardising acceptance of any possible continuation of the input word. Our results show that the history-deterministic (HD) VASS sit strictly between deterministic and non-deterministic VASS regardless of the number of counters. We compare the relative expressiveness of HD systems, and closure-properties of the induced language classes, with coverability and reachability semantics, and with and without ε-labelled transitions. Whereas in dimension 1, inclusion and regularity remain decidable, from dimension two onwards, HD-VASS with suitable resolver strategies, are essentially able to simulate 2-counter Minsky machines, leading to several undecidability results: It is undecidable whether a VASS is history-deterministic, or if a language equivalent history-deterministic VASS exists. Checking language inclusion between history-deterministic 2-VASS is also undecidable.

Cite as

Sougata Bose, David Purser, and Patrick Totzke. History-Deterministic Vector Addition Systems. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.CONCUR.2023.18,
  author =	{Bose, Sougata and Purser, David and Totzke, Patrick},
  title =	{{History-Deterministic Vector Addition Systems}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{18:1--18: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.18},
  URN =		{urn:nbn:de:0030-drops-190120},
  doi =		{10.4230/LIPIcs.CONCUR.2023.18},
  annote =	{Keywords: Vector Addition Systems, History-determinism, Good-for Games}
}
Document
Invited Talk
A Brief History of History-Determinism (Invited Talk)

Authors: Karoliina Lehtinen

Published in: LIPIcs, Volume 254, 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)


Abstract
Most nondeterministic automata models are more expressive, or at least more succinct, than their deterministic counterparts; however, this comes at a cost, as deterministic automata tend to have better algorithmic properties. History-deterministic automata are an intermediate model that allows a restricted form of nondeterminism: all nondeterministic choices must be resolvable on-the-fly, with only the knowledge of the word prefix read so far - as opposed to general nondeterminism, which allows for guessing the future of the word. History-deterministic automata combine some of the algorithmic benefits of determinism with some of the increased power of nondeterminism, thus enjoying (some of) the best of both worlds. History-determinism, as it is understood today, has its roots in several independently invented notions: Kupferman, Safra and Vardi’s automata recognising tree languages derived from word languages [Kupferman et al., 2006] (a notion that has been later referred to as automata that are good-for-trees [Udi Boker et al., 2013]), Henzinger and Piterman’s good-for-games automata [Thomas Henzinger and Nir Piterman, 2006], and Colcombet’s history-deterministic automata, introduced in his work on regular cost-automata [Colcombet, 2009]. In the ω-regular setting, where they were initially most studied, the notions of good-for-trees, good-for-games and history-determinism are equivalent, despite differences in their definitions. The key algorithmic appeal of these automata is that like deterministic automata, they have good compositional properties. This makes them particularly useful for applications such as reactive synthesis, where composition of games and automata is at the heart of effective solutions. Since then, history-determinism has received its fair share of attention, not least because of its relevance to synthesis. Indeed it turns out to be a natural and useful form of nondeterminism more broadly, and can be generalised to all sorts of different automata models: alternating automata [Udi Boker and Karoliina Lehtinen, 2019], pushdown automata [Enzo Erlich et al., 2022; Enzo Erlich et al., 2022], timed automata [Thomas A. Henzinger et al., 2022; Sougata Bose et al., 2022], Parikh automata [Enzo Erlich et al., 2022], and quantiative automata [Udi Boker and Karoliina Lehtinen, 2021], to name a few. In each of these models, history-determinism offers some trade-offs between the power of nondeterminism and the algorithmic properties of determinism. In particular, depending on the model, they can be either more expressive or more succinct than their deterministic counterparts, while retaining better algorithmic properties - in particular with respect to deciding universality, language inclusion and games - than fully nondeterministic automata. The drive to extend history-determinism to more powerful automata models has also lead to a better understanding of the properties of these automata, of how they compare to related notions (such as good-for-games automata and determinisability by pruning), and of the various games and tools used to study them. This talk aims to give a broad introduction to the notion of history determinism as well as an overview of some of the recent developements on the topic. It will also highlight some of the many problems that remain open. It is loosely based on a recent survey, written jointly with Udi Boker, which gives an informal presentation of what are, in our view, the key aspects of history-determinism [Udi Boker and Karoliina Lehtinen, 2023].

Cite as

Karoliina Lehtinen. A Brief History of History-Determinism (Invited Talk). In 40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 254, pp. 1:1-1:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{lehtinen:LIPIcs.STACS.2023.1,
  author =	{Lehtinen, Karoliina},
  title =	{{A Brief History of History-Determinism}},
  booktitle =	{40th International Symposium on Theoretical Aspects of Computer Science (STACS 2023)},
  pages =	{1:1--1:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-266-2},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{254},
  editor =	{Berenbrink, Petra and Bouyer, Patricia and Dawar, Anuj and Kant\'{e}, Mamadou Moustapha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2023.1},
  URN =		{urn:nbn:de:0030-drops-176535},
  doi =		{10.4230/LIPIcs.STACS.2023.1},
  annote =	{Keywords: History-determinism, nondeterminism, automata, good-for-games}
}
Document
On Synthesis of Resynchronizers for Transducers

Authors: Sougata Bose, Shankara Narayanan Krishna, Anca Muscholl, Vincent Penelle, and Gabriele Puppis

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


Abstract
We study two formalisms that allow to compare transducers over words under origin semantics: rational and regular resynchronizers, and show that the former are captured by the latter. We then consider some instances of the following synthesis problem: given transducers T_1,T_2, construct a rational (resp. regular) resynchronizer R, if it exists, such that T_1 is contained in R(T_2) under the origin semantics. We show that synthesis of rational resynchronizers is decidable for functional, and even finite-valued, one-way transducers, and undecidable for relational one-way transducers. In the two-way setting, synthesis of regular resynchronizers is shown to be decidable for unambiguous two-way transducers. For larger classes of two-way transducers, the decidability status is open.

Cite as

Sougata Bose, Shankara Narayanan Krishna, Anca Muscholl, Vincent Penelle, and Gabriele Puppis. On Synthesis of Resynchronizers for Transducers. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 69:1-69:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.MFCS.2019.69,
  author =	{Bose, Sougata and Krishna, Shankara Narayanan and Muscholl, Anca and Penelle, Vincent and Puppis, Gabriele},
  title =	{{On Synthesis of Resynchronizers for Transducers}},
  booktitle =	{44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019)},
  pages =	{69:1--69: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2019.69},
  URN =		{urn:nbn:de:0030-drops-110133},
  doi =		{10.4230/LIPIcs.MFCS.2019.69},
  annote =	{Keywords: String transducers, resynchronizers, synthesis}
}
Document
Origin-Equivalence of Two-Way Word Transducers Is in PSPACE

Authors: Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)


Abstract
We consider equivalence and containment problems for word transductions. These problems are known to be undecidable when the transductions are relations between words realized by non-deterministic transducers, and become decidable when restricting to functions from words to words. Here we prove that decidability can be equally recovered the origin semantics, that was introduced by Bojanczyk in 2014. We prove that the equivalence and containment problems for two-way word transducers in the origin semantics are PSPACE-complete. We also consider a variant of the containment problem where two-way transducers are compared under the origin semantics, but in a more relaxed way, by allowing distortions of the origins. The possible distortions are described by means of a resynchronization relation. We propose MSO-definable resynchronizers and show that they preserve the decidability of the containment problem under resynchronizations. {}

Cite as

Sougata Bose, Anca Muscholl, Vincent Penelle, and Gabriele Puppis. Origin-Equivalence of Two-Way Word Transducers Is in PSPACE. In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


Copy BibTex To Clipboard

@InProceedings{bose_et_al:LIPIcs.FSTTCS.2018.22,
  author =	{Bose, Sougata and Muscholl, Anca and Penelle, Vincent and Puppis, Gabriele},
  title =	{{Origin-Equivalence of Two-Way Word Transducers Is in PSPACE}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.22},
  URN =		{urn:nbn:de:0030-drops-99213},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.22},
  annote =	{Keywords: Transducers, origin semantics, equivalence}
}
  • Refine by Author
  • 3 Bose, Sougata
  • 2 Muscholl, Anca
  • 2 Penelle, Vincent
  • 2 Puppis, Gabriele
  • 1 Krishna, Shankara Narayanan
  • Show More...

  • Refine by Classification
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Transducers

  • Refine by Keyword
  • 2 History-determinism
  • 1 Good-for Games
  • 1 String transducers
  • 1 Transducers
  • 1 Vector Addition Systems
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2018
  • 1 2019

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