DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2023.19

Synchronized CTL over One-Counter Automata

Authors: Shaull Almagor, Daniel Assa, and Udi Boker

Published in: LIPIcs, Volume 284, 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)

Abstract

We consider the model-checking problem of Synchronized Computation-Tree Logic (CTL+Sync) over One-Counter Automata (OCAs). CTL+Sync augments CTL with temporal operators that require several paths to satisfy properties in a synchronous manner, e.g., the property "all paths should eventually see p at the same time". The model-checking problem for CTL+Sync over finite-state Kripke structures was shown to be in 𝖯^{NP^NP}. OCAs are labelled transition systems equipped with a non-negative counter that can be zero-tested. Thus, they induce infinite-state systems whose computation trees are not regular. The model-checking problem for CTL over OCAs was shown to be PSPACE-complete. We show that the model-checking problem for CTL+Sync over OCAs is decidable. However, the upper bound we give is non-elementary. We therefore proceed to study the problem for a central fragment of CTL+Sync, extending CTL with operators that require all paths to satisfy properties in a synchronous manner, and show that it is in EXP^NEXP (and in particular in EXPSPACE), by exhibiting a certain "segmented periodicity" in the computation trees of OCAs.

Cite as

Shaull Almagor, Daniel Assa, and Udi Boker. Synchronized CTL over One-Counter Automata. In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, pp. 19:1-19:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2023.19,
  author =	{Almagor, Shaull and Assa, Daniel and Boker, Udi},
  title =	{{Synchronized CTL over One-Counter Automata}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{19:1--19:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-304-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{284},
  editor =	{Bouyer, Patricia and Srinivasan, Srikanth},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.19},
  URN =		{urn:nbn:de:0030-drops-193921},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.19},
  annote =	{Keywords: CTL, Synchronization, One Counter Automata, Model Checking}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2023.17

Safety and Liveness of Quantitative Automata

Authors: Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç

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

Abstract

The safety-liveness dichotomy is a fundamental concept in formal languages which plays a key role in verification. Recently, this dichotomy has been lifted to quantitative properties, which are arbitrary functions from infinite words to partially-ordered domains. We look into harnessing the dichotomy for the specific classes of quantitative properties expressed by quantitative automata. These automata contain finitely many states and rational-valued transition weights, and their common value functions Inf, Sup, LimInf, LimSup, LimInfAvg, LimSupAvg, and DSum map infinite words into the totally-ordered domain of real numbers. In this automata-theoretic setting, we establish a connection between quantitative safety and topological continuity and provide an alternative characterization of quantitative safety and liveness in terms of their boolean counterparts. For all common value functions, we show how the safety closure of a quantitative automaton can be constructed in PTime, and we provide PSpace-complete checks of whether a given quantitative automaton is safe or live, with the exception of LimInfAvg and LimSupAvg automata, for which the safety check is in ExpSpace. Moreover, for deterministic Sup, LimInf, and LimSup automata, we give PTime decompositions into safe and live automata. These decompositions enable the separation of techniques for safety and liveness verification for quantitative specifications.

Cite as

Udi Boker, Thomas A. Henzinger, Nicolas Mazzocchi, and N. Ege Saraç. Safety and Liveness of Quantitative Automata. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.CONCUR.2023.17,
  author =	{Boker, Udi and Henzinger, Thomas A. and Mazzocchi, Nicolas and Sara\c{c}, N. Ege},
  title =	{{Safety and Liveness of Quantitative Automata}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{17:1--17: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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2023.17},
  URN =		{urn:nbn:de:0030-drops-190118},
  doi =		{10.4230/LIPIcs.CONCUR.2023.17},
  annote =	{Keywords: quantitative safety, quantitative liveness, quantitative automata}
}

Document

Invited Talk

DOI: 10.4230/LIPIcs.STACS.2023.1

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

Invited Talk

DOI: 10.4230/LIPIcs.CSL.2022.1

Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk)

Authors: Udi Boker

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

Abstract

There is a challenging trade-off between deterministic and nondeterministic automata, where the former suit various applications better, however at the cost of being exponentially larger or even less expressive. This gave birth to many notions in between determinism and nondeterminism, aiming at enjoying, sometimes, the best of both worlds. Some of the notions are yes/no ones, for example initial nondeterminism (restricting nondeterminism to allowing several initial states), and some provide a measure of nondeterminism, for example the ambiguity level. We analyze the possible generalization of such notions from Boolean to quantitative automata, and suggest that it depends on the following key characteristics of the considered notion 𝖭 - whether it is syntactic or semantic, and if semantic, whether it is word-based or language-based. A syntactic notion, such as initial nondeterminism, applies as is to a quantitative automaton A, namely 𝖭(A). A word-based semantic notion, such as unambiguity, applies as is to a Boolean automaton t-A that is derived from A by accompanying it with some threshold value t ∈ ℝ, namely 𝖭(t-A). A language-based notion, such as history determinism, also applies as is to t-A, while in addition, it naturally generalizes into two different notions with respect to A itself, by either: i) taking the supremum of 𝖭(t-A) over all thresholds t, denoted by Threshold-𝖭(A); or ii) generalizing the basis of the notion from a language to a function, denoted simply by 𝖭(A). While in general 𝖭(A) ⇒ Threshold-𝖭(A) ⇒ 𝖭(t-A), we have for some notions 𝖭(A) ≡ Threshold-𝖭(A), and for some not. (For measure notions, ⇒ stands for ≥ with respect to the nondeterminism level.) We classify numerous notions known in the Boolean setting according to their characterization above, generalize them to the quantitative setting and look into relations between them. The generalized notions open new research directions with respect to quantitative automata, and provide insights on the original notions with respect to Boolean automata.

Cite as

Udi Boker. Between Deterministic and Nondeterministic Quantitative Automata (Invited Talk). In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 1:1-1:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{boker:LIPIcs.CSL.2022.1,
  author =	{Boker, Udi},
  title =	{{Between Deterministic and Nondeterministic Quantitative Automata}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{1:1--1:15},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.1},
  URN =		{urn:nbn:de:0030-drops-157218},
  doi =		{10.4230/LIPIcs.CSL.2022.1},
  annote =	{Keywords: Quantitative Automata, Measure of Nondeterminism, Determinism}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2021.38

History Determinism vs. Good for Gameness in Quantitative Automata

Authors: Udi Boker and Karoliina Lehtinen

Published in: LIPIcs, Volume 213, 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)

Abstract

Automata models between determinism and nondeterminism/alternations can retain some of the algorithmic properties of deterministic automata while enjoying some of the expressiveness and succinctness of nondeterminism. We study three closely related such models - history determinism, good for gameness and determinisability by pruning - on quantitative automata. While in the Boolean setting, history determinism and good for gameness coincide, we show that this is no longer the case in the quantitative setting: good for gameness is broader than history determinism, and coincides with a relaxed version of it, defined with respect to thresholds. We further identify criteria in which history determinism, which is generally broader than determinisability by pruning, coincides with it, which we then apply to typical quantitative automata types. As a key application of good for games and history deterministic automata is synthesis, we clarify the relationship between the two notions and various quantitative synthesis problems. We show that good-for-games automata are central for "global" (classical) synthesis, while "local" (good-enough) synthesis reduces to deciding whether a nondeterministic automaton is history deterministic.

Cite as

Udi Boker and Karoliina Lehtinen. History Determinism vs. Good for Gameness in Quantitative Automata. In 41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 213, pp. 38:1-38:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2021.38,
  author =	{Boker, Udi and Lehtinen, Karoliina},
  title =	{{History Determinism vs. Good for Gameness in Quantitative Automata}},
  booktitle =	{41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
  pages =	{38:1--38:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-215-0},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{213},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Chekuri, Chandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2021.38},
  URN =		{urn:nbn:de:0030-drops-155495},
  doi =		{10.4230/LIPIcs.FSTTCS.2021.38},
  annote =	{Keywords: Good for games, history determinism, alternation, quantitative automata}
}

Document

DOI: 10.4230/LIPIcs.CSL.2021.12

Discounted-Sum Automata with Multiple Discount Factors

Authors: Udi Boker and Guy Hefetz

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract

Discounting the influence of future events is a key paradigm in economics and it is widely used in computer-science models, such as games, Markov decision processes (MDPs), reinforcement learning, and automata. While a single game or MDP may allow for several different discount factors, discounted-sum automata (NDAs) were only studied with respect to a single discount factor. For every integer λ ∈ ℕ⧵{0,1}, as opposed to every λ ∈ ℚ⧵ℕ, the class of NDAs with discount factor λ (λ-NDAs) has good computational properties: it is closed under determinization and under the algebraic operations min, max, addition, and subtraction, and there are algorithms for its basic decision problems, such as automata equivalence and containment. We define and analyze discounted-sum automata in which each transition can have a different integral discount factor (integral NMDAs). We show that integral NMDAs with an arbitrary choice of discount factors are not closed under determinization and under algebraic operations. We then define and analyze a restricted class of integral NMDAs, which we call tidy NMDAs, in which the choice of discount factors depends on the prefix of the word read so far. Tidy NMDAs are as expressive as deterministic integral NMDAs with an arbitrary choice of discount factors, and some of their special cases are NMDAs in which the discount factor depends on the action (alphabet letter) or on the elapsed time. We show that for every function θ that defines the choice of discount factors, the class of θ-NMDAs enjoys all of the above good properties of integral NDAs, as well as the same complexities of the required decision problems. To this end, we also improve the previously known complexities of the decision problems of integral NDAs, and present tight bounds on the size blow-up involved in algebraic operations on them. All our results hold equally for automata on finite words and for automata on infinite words.

Cite as

Udi Boker and Guy Hefetz. Discounted-Sum Automata with Multiple Discount Factors. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 12:1-12:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.CSL.2021.12,
  author =	{Boker, Udi and Hefetz, Guy},
  title =	{{Discounted-Sum Automata with Multiple Discount Factors}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{12:1--12:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.12},
  URN =		{urn:nbn:de:0030-drops-134468},
  doi =		{10.4230/LIPIcs.CSL.2021.12},
  annote =	{Keywords: Automata, Discounted-sum, Quantitative verification, NMDA, NDA}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2020.41

On the Succinctness of Alternating Parity Good-For-Games Automata

Authors: Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak

Published in: LIPIcs, Volume 182, 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)

Abstract

We study alternating parity good-for-games (GFG) automata, i.e., alternating parity automata where both conjunctive and disjunctive choices can be resolved in an online manner, without knowledge of the suffix of the input word still to be read. We show that they can be exponentially more succinct than both their nondeterministic and universal counterparts. Furthermore, we present a single exponential determinisation procedure and an Exptime upper bound to the problem of recognising whether an alternating automaton is GFG. We also study the complexity of deciding "half-GFGness", a property specific to alternating automata that only requires nondeterministic choices to be resolved in an online manner. We show that this problem is PSpace-hard already for alternating automata on finite words.

Cite as

Udi Boker, Denis Kuperberg, Karoliina Lehtinen, and Michał Skrzypczak. On the Succinctness of Alternating Parity Good-For-Games Automata. In 40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 182, pp. 41:1-41:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2020.41,
  author =	{Boker, Udi and Kuperberg, Denis and Lehtinen, Karoliina and Skrzypczak, Micha{\l}},
  title =	{{On the Succinctness of Alternating Parity Good-For-Games Automata}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{41:1--41:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-174-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{182},
  editor =	{Saxena, Nitin and Simon, Sunil},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.41},
  URN =		{urn:nbn:de:0030-drops-132825},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.41},
  annote =	{Keywords: Good for games, history-determinism, alternation}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2020.47

Parametrized Universality Problems for One-Counter Nets

Authors: Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke

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

Abstract

We study the language universality problem for One-Counter Nets, also known as 1-dimensional Vector Addition Systems with States (1-VASS), parameterized either with an initial counter value, or with an upper bound on the allowed counter value during runs. The language accepted by an OCN (defined by reaching a final control state) is monotone in both parameters. This yields two natural questions: 1) does there exist an initial counter value that makes the language universal? 2) does there exist a sufficiently high ceiling so that the bounded language is universal? Although the ordinary universality problem is decidable (and Ackermann-complete) and these parameterized variants seem to reduce to checking basic structural properties of the underlying automaton, we show that in fact both problems are undecidable. We also look into the complexities of the problems for several decidable subclasses, namely for unambiguous, and deterministic systems, and for those over a single-letter alphabet.

Cite as

Shaull Almagor, Udi Boker, Piotr Hofman, and Patrick Totzke. Parametrized Universality Problems for One-Counter Nets. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 47:1-47:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2020.47,
  author =	{Almagor, Shaull and Boker, Udi and Hofman, Piotr and Totzke, Patrick},
  title =	{{Parametrized Universality Problems for One-Counter Nets}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{47:1--47:16},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.47},
  URN =		{urn:nbn:de:0030-drops-128592},
  doi =		{10.4230/LIPIcs.CONCUR.2020.47},
  annote =	{Keywords: Counter net, VASS, Unambiguous Automata, Universality}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2019.19

Good for Games Automata: From Nondeterminism to Alternation

Authors: Udi Boker and Karoliina Lehtinen

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract

A word automaton recognizing a language L is good for games (GFG) if its composition with any game with winning condition L preserves the game’s winner. While all deterministic automata are GFG, some nondeterministic automata are not. There are various other properties that are used in the literature for defining that a nondeterministic automaton is GFG, including "history-deterministic", "compliant with some letter game", "good for trees", and "good for composition with other automata". The equivalence of these properties has not been formally shown. We generalize all of these definitions to alternating automata and show their equivalence. We further show that alternating GFG automata are as expressive as deterministic automata with the same acceptance conditions and indices. We then show that alternating GFG automata over finite words, and weak automata over infinite words, are not more succinct than deterministic automata, and that determinizing Büchi and co-Büchi alternating GFG automata involves a 2^{Theta(n)} state blow-up. We leave open the question of whether alternating GFG automata of stronger acceptance conditions allow for doubly-exponential succinctness compared to deterministic automata.

Cite as

Udi Boker and Karoliina Lehtinen. Good for Games Automata: From Nondeterminism to Alternation. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 19:1-19:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.CONCUR.2019.19,
  author =	{Boker, Udi and Lehtinen, Karoliina},
  title =	{{Good for Games Automata: From Nondeterminism to Alternation}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{19:1--19:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.19},
  URN =		{urn:nbn:de:0030-drops-109212},
  doi =		{10.4230/LIPIcs.CONCUR.2019.19},
  annote =	{Keywords: Good for games, history-determinism, alternation}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2018.21

On the Way to Alternating Weak Automata

Authors: Udi Boker and Karoliina Lehtinen

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

Abstract

Different types of automata over words and trees offer different trade-offs between expressivity, conciseness, and the complexity of decision procedures. Alternating weak automata enjoy simple algorithms for emptiness and membership checks, which makes transformations into automata of this type particularly interesting. For instance, an algorithm for solving two-player infinite games can be viewed as a special case of such a transformation. However, our understanding of the worst-case size blow-up that these transformations can incur is rather poor. This paper establishes two new results, one on word automata and one on tree automata. We show that: - Alternating parity word automata can be turned into alternating weak automata of quasi-polynomial (rather than exponential) size. - Universal co-Büchi tree automata, a special case of alternating parity tree automata, can be exponentially more concise than alternating weak automata. Along the way, we present a family of game languages, strict for the levels of the weak hierarchy of tree automata, which corresponds to a weak version of the canonical game languages known to be strict for the Mostowski - Rabin index hierarchy.

Cite as

Udi Boker and Karoliina Lehtinen. On the Way to Alternating Weak Automata. 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. 21:1-21:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2018.21,
  author =	{Boker, Udi and Lehtinen, Karoliina},
  title =	{{On the Way to Alternating Weak Automata}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{21:1--21:22},
  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.21},
  URN =		{urn:nbn:de:0030-drops-99200},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.21},
  annote =	{Keywords: Alternating automata, Parity games, Parity automata, Weak automata}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.17

Rabin vs. Streett Automata

Authors: Udi Boker

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract

The Rabin and Streett acceptance conditions are dual. Accordingly, deterministic Rabin and Streett automata are dual. Yet, when adding nondeterminsim, the picture changes dramatically. In fact, the state blowup involved in translations between Rabin and Streett automata is a longstanding open problem, having an exponential gap between the known lower and upper bounds. We resolve the problem, showing that the translation of Streett to Rabin automata involves a state blowup in $\Theta(n^2)$, whereas in the other direction, the translations of both deterministic and nondeterministic Rabin automata to nondeterministic Streett automata involve a state blowup in $2^{\Theta(n)}$. Analyzing this substantial difference between the two directions, we get to the conclusion that when studying translations between automata, one should not only consider the state blowup, but also the \emph{size} blowup, where the latter takes into account all of the automaton elements. More precisely, the size of an automaton is defined to be the maximum of the alphabet length, the number of states, the number of transitions, and the acceptance condition length (index). Indeed, size-wise, the results are opposite. That is, the translation of Rabin to Streett involves a size blowup in $\Theta(n^2)$ and of Streett to Rabin in $2^{\Theta(n)}$. The core difference between state blowup and size blowup stems from the tradeoff between the index and the number of states. (Recall that the index of Rabin and Streett automata might be exponential in the number of states.) We continue with resolving the open problem of translating deterministic Rabin and Streett automata to the weaker types of deterministic co-B\"uchi and B\"uchi automata, respectively. We show that the state blowup involved in these translations, when possible, is in $2^{\Theta(n)}$, whereas the size blowup is in $\Theta(n^2)$.

Cite as

Udi Boker. Rabin vs. Streett Automata. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{boker:LIPIcs.FSTTCS.2017.17,
  author =	{Boker, Udi},
  title =	{{Rabin vs. Streett Automata}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{17:1--17:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.17},
  URN =		{urn:nbn:de:0030-drops-83782},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.17},
  annote =	{Keywords: Finite automata on infinite words, translations, automata size, state space}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2017.18

How Deterministic are Good-For-Games Automata?

Authors: Udi Boker, Orna Kupferman, and Michal Skrzypczak

Published in: LIPIcs, Volume 93, 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)

Abstract

In good for games (GFG) automata, it is possible to resolve nondeterminism in a way that only depends on the past and still accepts all the words in the language. The motivation for GFG automata comes from their adequacy for games and synthesis, wherein general nondeterminism is inappropriate. We continue the ongoing effort of studying the power of nondeterminism in GFG automata. Initial indications have hinted that every GFG automaton embodies a deterministic one. Today we know that this is not the case, and in fact GFG automata may be exponentially more succinct than deterministic ones. We focus on the typeness question, namely the question of whether a GFG automaton with a certain acceptance condition has an equivalent GFG automaton with a weaker acceptance condition on the same structure. Beyond the theoretical interest in studying typeness, its existence implies efficient translations among different acceptance conditions. This practical issue is of special interest in the context of games, where the Büchi and co-Büchi conditions admit memoryless strategies for both players. Typeness is known to hold for deterministic automata and not to hold for general nondeterministic automata. We show that GFG automata enjoy the benefits of typeness, similarly to the case of deterministic automata. In particular, when Rabin or Streett GFG automata have equivalent Büchi or co-Büchi GFG automata, respectively, then such equivalent automata can be defined on a substructure of the original automata. Using our typeness results, we further study the place of GFG automata in between deterministic and nondeterministic ones. Specifically, considering automata complementation, we show that GFG automata lean toward nondeterministic ones, admitting an exponential state blow-up in the complementation of a Streett automaton into a Rabin automaton, as opposed to the constant blow-up in the deterministic case.

Cite as

Udi Boker, Orna Kupferman, and Michal Skrzypczak. How Deterministic are Good-For-Games Automata?. In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 93, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2017.18,
  author =	{Boker, Udi and Kupferman, Orna and Skrzypczak, Michal},
  title =	{{How Deterministic are Good-For-Games Automata?}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{18:1--18:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-055-2},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{93},
  editor =	{Lokam, Satya and Ramanujam, R.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.18},
  URN =		{urn:nbn:de:0030-drops-83776},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.18},
  annote =	{Keywords: finite automata on infinite words, determinism, good-for-games}
}

Document

DOI: 10.4230/LIPIcs.CSL.2017.12

On the (In)Succinctness of Muller Automata

Authors: Udi Boker

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract

There are several types of finite automata on infinite words, differing in their acceptance conditions. As each type has its own advantages, there is an extensive research on the size blowup involved in translating one automaton type to another. Of special interest is the Muller type, providing the most detailed acceptance condition. It turns out that there is inconsistency and incompleteness in the literature results regarding the translations to and from Muller automata. Considering the automaton size, some results take into account, in addition to the number of states, the alphabet length and the number of transitions while ignoring the length of the acceptance condition, whereas other results consider the length of the acceptance condition while ignoring the two other parameters. We establish a full picture of the translations to and from Muller automata, enhancing known results and adding new ones. Overall, Muller automata can be considered less succinct than parity, Rabin, and Streett automata: translating nondeterministic Muller automata to the other nondeterministic types involves a polynomial size blowup, while the other way round is exponential; translating between the deterministic versions is exponential in both directions; and translating nondeterministic automata of all types to deterministic Muller automata is doubly exponential, as opposed to a single exponent in the translations to the other deterministic types.

Cite as

Udi Boker. On the (In)Succinctness of Muller Automata. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 12:1-12:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{boker:LIPIcs.CSL.2017.12,
  author =	{Boker, Udi},
  title =	{{On the (In)Succinctness of Muller Automata}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{12:1--12:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.12},
  URN =		{urn:nbn:de:0030-drops-76751},
  doi =		{10.4230/LIPIcs.CSL.2017.12},
  annote =	{Keywords: Automata, Omega-regular languages, Determinization}
}

Document

DOI: 10.4230/LIPIcs.MFCS.2016.11

Families of DFAs as Acceptors of omega-Regular Languages

Authors: Dana Angluin, Udi Boker, and Dana Fisman

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

Abstract

Families of DFAs (FDFAs) provide an alternative formalism for recognizing omega-regular languages. The motivation for introducing them was a desired correlation between the automaton states and right congruence relations, in a manner similar to the Myhill-Nerode theorem for regular languages. This correlation is beneficial for learning algorithms, and indeed it was recently shown that omega-regular languages can be learned from membership and equivalence queries, using FDFAs as the acceptors. In this paper, we look into the question of how suitable FDFAs are for defining omega-regular languages. Specifically, we look into the complexity of performing Boolean operations, such as complementation and intersection, on FDFAs, the complexity of solving decision problems, such as emptiness and language containment, and the succinctness of FDFAs compared to standard deterministic and nondeterministic omega-automata. We show that FDFAs enjoy the benefits of deterministic automata with respect to Boolean operations and decision problems. Namely, they can all be performed in nondeterministic logarithmic space. We provide polynomial translations of deterministic Buchi and coBuchi automata to FDFAs and of FDFAs to nondeterministic Buchi automata (NBAs). We show that translation of an NBA to an FDFA may involve an exponential blowup. Last, we show that FDFAs are more succinct than deterministic parity automata (DPAs) in the sense that translating a DPA to an FDFA can always be done with only a polynomial increase, yet the other direction involves an inevitable exponential blowup in the worst case.

Cite as

Dana Angluin, Udi Boker, and Dana Fisman. Families of DFAs as Acceptors of omega-Regular Languages. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 11:1-11:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{angluin_et_al:LIPIcs.MFCS.2016.11,
  author =	{Angluin, Dana and Boker, Udi and Fisman, Dana},
  title =	{{Families of DFAs as Acceptors of omega-Regular Languages}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{11:1--11:14},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2016.11},
  URN =		{urn:nbn:de:0030-drops-64274},
  doi =		{10.4230/LIPIcs.MFCS.2016.11},
  annote =	{Keywords: finite automata, omega regular languages}
}

Document

DOI: 10.4230/LIPIcs.FSTTCS.2012.362

Approximate Determinization of Quantitative Automata

Authors: Udi Boker and Thomas A. Henzinger

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

Abstract

Quantitative automata are nondeterministic finite automata with edge weights. They value a run by some function from the sequence of visited weights to the reals, and value a word by its minimal/maximal run. They generalize boolean automata, and have gained much attention in recent years. Unfortunately, important automaton classes, such as sum, discounted-sum, and limit-average automata, cannot be determinized. Yet, the quantitative setting provides the potential of approximate determinization. We define approximate determinization with respect to a distance function, and investigate this potential. We show that sum automata cannot be determinized approximately with respect to any distance function. However, restricting to nonnegative weights allows for approximate determinization with respect to some distance functions. Discounted-sum automata allow for approximate determinization, as the influence of a word's suffix is decaying. However, the naive approach, of unfolding the automaton computations up to a sufficient level, is shown to be doubly exponential in the discount factor. We provide an alternative construction that is singly exponential in the discount factor, in the precision, and in the number of states. We prove matching lower bounds, showing exponential dependency on each of these three parameters. Average and limit-average automata are shown to prohibit approximate determinization with respect to any distance function, and this is the case even for two weights, 0 and 1.

Cite as

Udi Boker and Thomas A. Henzinger. Approximate Determinization of Quantitative Automata. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 362-373, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2012.362,
  author =	{Boker, Udi and Henzinger, Thomas A.},
  title =	{{Approximate Determinization of Quantitative Automata}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{362--373},
  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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.362},
  URN =		{urn:nbn:de:0030-drops-38739},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.362},
  annote =	{Keywords: Quantitative; Automata; Determinization; Approximation}
}

17 Search Results for "Boker, Udi"

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Abstract

Cite as

Thanks for your feedback!

Could not send message