4 Search Results for "Leshkowitz, Ofer"

Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2024.124
Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata

Authors: Rohan Acharya, Marcin Jurdziński, and Aditya Prakash

Published in: LIPIcs, Volume 297, 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)

Abstract
Our main technical contribution is a polynomial-time determinisation procedure for history-deterministic Büchi automata, which settles an open question of Kuperberg and Skrzypczak, 2015. A key conceptual contribution is the lookahead game, which is a variant of Bagnol and Kuperberg’s token game, in which Adam is given a fixed lookahead. We prove that the lookahead game is equivalent to the 1-token game. This allows us to show that the 1-token game characterises history-determinism for semantically-deterministic Büchi automata, which paves the way to our polynomial-time determinisation procedure.
Cite as

Rohan Acharya, Marcin Jurdziński, and Aditya Prakash. Lookahead Games and Efficient Determinisation of History-Deterministic Büchi Automata. In 51st International Colloquium on Automata, Languages, and Programming (ICALP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 297, pp. 124:1-124:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{acharya_et_al:LIPIcs.ICALP.2024.124,
  author =	{Acharya, Rohan and Jurdzi\'{n}ski, Marcin and Prakash, Aditya},
  title =	{{Lookahead Games and Efficient Determinisation of History-Deterministic B\"{u}chi Automata}},
  booktitle =	{51st International Colloquium on Automata, Languages, and Programming (ICALP 2024)},
  pages =	{124:1--124:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-322-5},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{297},
  editor =	{Bringmann, Karl and Grohe, Martin and Puppis, Gabriele and Svensson, Ola},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2024.124},
  URN =		{urn:nbn:de:0030-drops-202672},
  doi =		{10.4230/LIPIcs.ICALP.2024.124},
  annote =	{Keywords: History determinism, Good-for-games, Automata over infinite words, Games}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.42
Synthesis of Privacy-Preserving Systems

Authors: Orna Kupferman and Ofer Leshkowitz

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

Abstract
Synthesis is the automated construction of a system from its specification. In many cases, we want to maintain the privacy of the system and the environment, thus limit the information that they share with each other or with an observer of the interaction. We introduce a framework for synthesis that addresses privacy in a simple yet powerful way. Our method is based on specification formalisms that include an unknown truth value. When the system and the environment interact, they may keep the truth values of some input and output signals private, which may cause the satisfaction value of specifications to become unknown. The input to the synthesis problem contains, in addition to the specification φ, also secrets ψ_1,…,ψ_k. During the interaction, the system directs the environment which input signals should stay private. The system then realizes the specification if in all interactions, the satisfaction value of the specification φ is true, whereas the satisfaction value of the secrets ψ_1,…,ψ_k is unknown. Thus, the specification is satisfied without the secrets being revealed. We describe our framework for specifications and secrets in LTL, and extend the framework also to the multi-valued specification formalism LTL[F], which enables the specification of the quality of computations. When both the specification and secrets are in LTL[F], one can trade-off the satisfaction value of the specification with the extent to which the satisfaction values of the secrets are revealed. We show that the complexity of the problem in all settings is 2EXPTIME-complete, thus it is not harder than synthesis with no privacy requirements.
Cite as

Orna Kupferman and Ofer Leshkowitz. Synthesis of Privacy-Preserving Systems. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 42:1-42:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2022.42,
  author =	{Kupferman, Orna and Leshkowitz, Ofer},
  title =	{{Synthesis of Privacy-Preserving Systems}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{42:1--42:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.42},
  URN =		{urn:nbn:de:0030-drops-174342},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.42},
  annote =	{Keywords: Synthesis, Privacy, LTL, Games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2021.85
A Hierarchy of Nondeterminism

Authors: Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz

Published in: LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)

Abstract
We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton A is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to A by removing some of its transitions. Then, A is good-for-games (GFG) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, A is semantically deterministic (SD) if different nondeterministic choices in A lead to equivalent states. Some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism. For example, DBP automata are useful in the analysis of online algorithms, and GFG automata are useful in synthesis and control. For automata on finite words, the three levels in the hierarchy coincide. We study the hierarchy for Büchi, co-Büchi, and weak automata on infinite words. We show that the hierarchy is strict, study the expressive power of the different levels in it, as well as the complexity of deciding the membership of a language in a given level. Finally, we describe a probability-based analysis of the hierarchy, which relates the level of nondeterminism with the probability that a random run on a word in the language is accepting.
Cite as

Bader Abu Radi, Orna Kupferman, and Ofer Leshkowitz. A Hierarchy of Nondeterminism. In 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 202, pp. 85:1-85:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{aburadi_et_al:LIPIcs.MFCS.2021.85,
  author =	{Abu Radi, Bader and Kupferman, Orna and Leshkowitz, Ofer},
  title =	{{A Hierarchy of Nondeterminism}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{85:1--85:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.85},
  URN =		{urn:nbn:de:0030-drops-145254},
  doi =		{10.4230/LIPIcs.MFCS.2021.85},
  annote =	{Keywords: Automata on Infinite Words, Expressive power, Complexity, Games}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.59
On Repetition Languages

Authors: Orna Kupferman and Ofer Leshkowitz

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
A regular language R of finite words induces three repetition languages of infinite words: the language lim(R), which contains words with infinitely many prefixes in R, the language ∞ R, which contains words with infinitely many disjoint subwords in R, and the language R^ω, which contains infinite concatenations of words in R. Specifying behaviors, the three repetition languages provide three different ways of turning a specification of a finite behavior into an infinite one. We study the expressive power required for recognizing repetition languages, in particular whether they can always be recognized by a deterministic Büchi word automaton (DBW), the blow up in going from an automaton for R to automata for the repetition languages, and the complexity of related decision problems. For lim R and ∞ R, most of these problems have already been studied or are easy. We focus on R^ω. Its study involves some new and interesting results about additional repetition languages, in particular R^#, which contains exactly all words with unboundedly many concatenations of words in R. We show that R^ω is DBW-recognizable iff R^# is ω-regular iff R^# = R^ω, and there are languages for which these criteria do not hold. Thus, R^ω need not be DBW-recognizable. In addition, when exists, the construction of a DBW for R^ω may involve a 2^{O(n log n)} blow-up, and deciding whether R^ω is DBW-recognizable, for R given by a nondeterministic automaton, is PSPACE-complete. Finally, we lift the difference between R^# and R^ω to automata on finite words and study a variant of Büchi automata where a word is accepted if (possibly different) runs on it visit accepting states unboundedly many times.
Cite as

Orna Kupferman and Ofer Leshkowitz. On Repetition Languages. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 59:1-59:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.MFCS.2020.59,
  author =	{Kupferman, Orna and Leshkowitz, Ofer},
  title =	{{On Repetition Languages}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{59:1--59:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.59},
  URN =		{urn:nbn:de:0030-drops-127268},
  doi =		{10.4230/LIPIcs.MFCS.2020.59},
  annote =	{Keywords: B\"{u}chi automata, Expressive power, Succinctness}
}
  • Refine by Author
  • 3 Kupferman, Orna
  • 3 Leshkowitz, Ofer
  • 1 Abu Radi, Bader
  • 1 Acharya, Rohan
  • 1 Jurdziński, Marcin
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Automata over infinite objects
  • 1 Theory of computation

  • Refine by Keyword
  • 3 Games
  • 2 Expressive power
  • 1 Automata on Infinite Words
  • 1 Automata over infinite words
  • 1 Büchi automata
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 1 2020
  • 1 2021
  • 1 2022
  • 1 2024

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact