Search Results

Documents authored by Kupferman, Orna

Document
Complete Volume
DOI: 10.4230/LIPIcs.STACS.2024
LIPIcs, Volume 289, STACS 2024, Complete Volume

Authors: Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
LIPIcs, Volume 289, STACS 2024, Complete Volume
Cite as

41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 1-1048, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{beyersdorff_et_al:LIPIcs.STACS.2024,
  title =	{{LIPIcs, Volume 289, STACS 2024, Complete Volume}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{1--1048},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024},
  URN =		{urn:nbn:de:0030-drops-197098},
  doi =		{10.4230/LIPIcs.STACS.2024},
  annote =	{Keywords: LIPIcs, Volume 289, STACS 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.STACS.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Olaf Beyersdorff, Mamadou Moustapha Kanté, Orna Kupferman, and Daniel Lokshtanov

Published in: LIPIcs, Volume 289, 41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 289, pp. 0:i-0:xx, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{beyersdorff_et_al:LIPIcs.STACS.2024.0,
  author =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{41st International Symposium on Theoretical Aspects of Computer Science (STACS 2024)},
  pages =	{0:i--0:xx},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-311-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{289},
  editor =	{Beyersdorff, Olaf and Kant\'{e}, Mamadou Moustapha and Kupferman, Orna and Lokshtanov, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2024.0},
  URN =		{urn:nbn:de:0030-drops-197108},
  doi =		{10.4230/LIPIcs.STACS.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2023.26
Monotonicity Characterizations of Regular Languages

Authors: Yoav Feinstein and Orna Kupferman

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

Abstract
Each language L ⊆ Σ^* induces an infinite sequence Pr(L,n)_{n=1}^∞, where for all n ≥ 1, the value Pr(L,n) ∈ [0,1] is the probability of a word of length n to be in L, assuming a uniform distribution on the letters in Σ. Previous studies of Pr(L,n)_{n=1}^∞ for a regular language L, concerned zero-one laws, density, and accumulation points. We study monotonicity of Pr(L,n)_{n=1}^∞, possibly in the limit. We show that monotonicity may depend on the distribution of letters, study how operations on languages affect monotonicity, and characterize classes of languages for which the sequence is monotonic. We extend the study to languages L of infinite words, where we study the probability of lasso-shaped words to be in L and consider two definitions for Pr(L,n). The first refers to the probability of prefixes of length n to be extended to words in L, and the second to the probability of word w of length n to be such that w^ω is in L. Thus, in the second definition, monotonicity depends not only on the length of w, but also on the words being periodic.
Cite as

Yoav Feinstein and Orna Kupferman. Monotonicity Characterizations of Regular Languages. 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. 26:1-26:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{feinstein_et_al:LIPIcs.FSTTCS.2023.26,
  author =	{Feinstein, Yoav and Kupferman, Orna},
  title =	{{Monotonicity Characterizations of Regular Languages}},
  booktitle =	{43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023)},
  pages =	{26:1--26:19},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2023.26},
  URN =		{urn:nbn:de:0030-drops-193998},
  doi =		{10.4230/LIPIcs.FSTTCS.2023.26},
  annote =	{Keywords: Regular Languages, Probability, Monotonicity, Automata}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2023.19
Games with Trading of Control

Authors: Orna Kupferman and Noam Shenwald

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

Abstract
The interaction among components in a system is traditionally modeled by a game. In the turned-based setting, the players in the game jointly move a token along the game graph, with each player deciding where to move the token in vertices she controls. The objectives of the players are modeled by ω-regular winning conditions, and players whose objectives are satisfied get rewards. Thus, the game is non-zero-sum, and we are interested in its stable outcomes. In particular, in the rational-synthesis problem, we seek a strategy for the system player that guarantees the satisfaction of the system’s objective in all rational environments. In this paper, we study an extension of the traditional setting by trading of control. In our game, the players may pay each other in exchange for directing the token also in vertices they do not control. The utility of each player then combines the reward for the satisfaction of her objective and the profit from the trading. The setting combines challenges from ω-regular graph games with challenges in pricing, bidding, and auctions in classical game theory. We study the theoretical properties of parity trading games: best-response dynamics, existence and search for Nash equilibria, and measures for equilibrium inefficiency. We also study the rational-synthesis problem and analyze its tight complexity in various settings.
Cite as

Orna Kupferman and Noam Shenwald. Games with Trading of Control. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2023.19,
  author =	{Kupferman, Orna and Shenwald, Noam},
  title =	{{Games with Trading of Control}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{19:1--19: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.19},
  URN =		{urn:nbn:de:0030-drops-190137},
  doi =		{10.4230/LIPIcs.CONCUR.2023.19},
  annote =	{Keywords: Parity Games, Rational Synthesis, Game Theory, Auctions}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.109
On Semantically-Deterministic Automata

Authors: Bader Abu Radi and Orna Kupferman

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
Nondeterminism is a fundamental notion in Theoretical Computer Science. A nondeterministic automaton is semantically deterministic (SD) if different nondeterministic choices in the automaton lead to equivalent states. Semantic determinism is interesting as it is a natural relaxation of determinism, and as some applications of automata in formal methods require deterministic automata, yet in fact can use automata with some level of nondeterminism, tightly related to semantic determinism. In the context of finite words, semantic determinism coincides with determinism, in the sense that every pruning of an SD automaton to a deterministic one results in an equivalent automaton. We study SD automata on infinite words, focusing on Büchi, co-Büchi, and weak automata. We show that there, while semantic determinism does not increase the expressive power, the combinatorial and computational properties of SD automata are very different from these of deterministic automata. In particular, SD Büchi and co-Büchi automata are exponentially more succinct than deterministic ones (in fact, also exponentially more succinct than history-deterministic automata), their complementation involves an exponential blow up, and decision procedures for them like universality and minimization are PSPACE-complete. For weak automata, we show that while an SD weak automaton need not be pruned to an equivalent deterministic one, it can be determinized to an equivalent deterministic weak automaton with the same state space, implying also efficient complementation and decision procedures for SD weak automata.
Cite as

Bader Abu Radi and Orna Kupferman. On Semantically-Deterministic Automata. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 109:1-109:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{aburadi_et_al:LIPIcs.ICALP.2023.109,
  author =	{Abu Radi, Bader and Kupferman, Orna},
  title =	{{On Semantically-Deterministic Automata}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{109:1--109:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.109},
  URN =		{urn:nbn:de:0030-drops-181610},
  doi =		{10.4230/LIPIcs.ICALP.2023.109},
  annote =	{Keywords: Automata on infinite words, Nondeterminism, Succinctness, Decision procedures}
}
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
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2022.1
CONCUR Test-Of-Time Award 2022 (Invited Paper)

Authors: Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
This short article recaps the purpose of the CONCUR Test-of-Time Award and presents the four papers that received the Award in 2022.
Cite as

Ilaria Castellani, Paul Gastin, Orna Kupferman, Mickael Randour, and Davide Sangiorgi. CONCUR Test-Of-Time Award 2022 (Invited Paper). In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1:1-1:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{castellani_et_al:LIPIcs.CONCUR.2022.1,
  author =	{Castellani, Ilaria and Gastin, Paul and Kupferman, Orna and Randour, Mickael and Sangiorgi, Davide},
  title =	{{CONCUR Test-Of-Time Award 2022}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1:1--1:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.1},
  URN =		{urn:nbn:de:0030-drops-170644},
  doi =		{10.4230/LIPIcs.CONCUR.2022.1},
  annote =	{Keywords: CONCUR Test-of-Time Award}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2022.19
Energy Games with Resource-Bounded Environments

Authors: Orna Kupferman and Naama Shamash Halevy

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
An energy game is played between two players, modeling a resource-bounded system and its environment. The players take turns moving a token along a finite graph. Each edge of the graph is labeled by an integer, describing an update to the energy level of the system that occurs whenever the edge is traversed. The system wins the game if it never runs out of energy. Different applications have led to extensions of the above basic setting. For example, addressing a combination of the energy requirement with behavioral specifications, researchers have studied richer winning conditions, and addressing systems with several bounded resources, researchers have studied games with multi-dimensional energy updates. All extensions, however, assume that the environment has no bounded resources. We introduce and study both-bounded energy games (BBEGs), in which both the system and the environment have multi-dimensional energy bounds. In BBEGs, each edge in the game graph is labeled by two integer vectors, describing updates to the multi-dimensional energy levels of the system and the environment. A system wins a BBEG if it never runs out of energy or if its environment runs out of energy. We show that BBEGs are determined, and that the problem of determining the winner in a given BBEG is decidable iff both the system and the environment have energy vectors of dimension 1. We also study how restrictions on the memory of the system and/or the environment as well as upper bounds on their energy levels influence the winner and the complexity of the problem.
Cite as

Orna Kupferman and Naama Shamash Halevy. Energy Games with Resource-Bounded Environments. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2022.19,
  author =	{Kupferman, Orna and Shamash Halevy, Naama},
  title =	{{Energy Games with Resource-Bounded Environments}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{19:1--19:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.19},
  URN =		{urn:nbn:de:0030-drops-170823},
  doi =		{10.4230/LIPIcs.CONCUR.2022.19},
  annote =	{Keywords: Energy Games, Infinite-State Systems, Decidability}
}
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.FSTTCS.2020.51
Perspective Games with Notifications

Authors: Orna Kupferman and Noam Shenwald

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

Abstract
A reactive system has to satisfy its specification in all environments. Accordingly, design of correct reactive systems corresponds to the synthesis of winning strategies in games that model the interaction between the system and its environment. The game is played on a graph whose vertices are partitioned among the players. The players jointly generate a path in the graph, with each player deciding the successor vertex whenever the path reaches a vertex she owns. The objective of the system player is to force the computation induced by the generated infinite path to satisfy a given specification. The traditional way of modelling uncertainty in such games is observation-based. There, uncertainty is longitudinal: the players partially observe all vertices in the history. Recently, researchers introduced perspective games, where uncertainty is transverse: players fully observe the vertices they own and have no information about the behavior of the computation between visits in such vertices. We introduce and study perspective games with notifications: uncertainty is still transverse, yet a player may be notified about events that happen between visits in vertices she owns. We distinguish between structural notifications, for example about visits in some vertices, and behavioral notifications, for example about the computation exhibiting a certain behavior. We study the theoretic properties of perspective games with notifications, and the problem of deciding whether a player has a winning perspective strategy. Such a strategy depends only on the visible history, which consists of both visits in vertices the player owns and notifications during visits in other vertices. We show that the problem is EXPTIME-complete for objectives given by a deterministic or universal parity automaton over an alphabet that labels the vertices of the game, and notifications given by a deterministic satellite, and is 2EXPTIME-complete for LTL objectives. In all cases, the complexity in the size of the graph and the satellite is polynomial - exponentially easier than games with observation-based partial visibility. We also analyze the complexity of the problem for richer types of satellites.
Cite as

Orna Kupferman and Noam Shenwald. Perspective Games with Notifications. 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. 51:1-51:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2020.51,
  author =	{Kupferman, Orna and Shenwald, Noam},
  title =	{{Perspective Games with Notifications}},
  booktitle =	{40th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2020)},
  pages =	{51:1--51:16},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2020.51},
  URN =		{urn:nbn:de:0030-drops-132928},
  doi =		{10.4230/LIPIcs.FSTTCS.2020.51},
  annote =	{Keywords: Games, Incomplete Information, Automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.51
Unary Prime Languages

Authors: Ismaël Jecker, Orna Kupferman, and Nicolas Mazzocchi

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

Abstract
A regular language L of finite words is composite if there are regular languages L₁,L₂,…,L_t such that L = ⋂_{i = 1}^t L_i and the index (number of states in a minimal DFA) of every language L_i is strictly smaller than the index of L. Otherwise, L is prime. Primality of regular languages was introduced and studied in [O. Kupferman and J. Mosheiff, 2015], where the complexity of deciding the primality of the language of a given DFA was left open, with a doubly-exponential gap between the upper and lower bounds. We study primality for unary regular languages, namely regular languages with a singleton alphabet. A unary language corresponds to a subset of ℕ, making the study of unary prime languages closer to that of primality in number theory. We show that the setting of languages is richer. In particular, while every composite number is the product of two smaller numbers, the number t of languages necessary to decompose a composite unary language induces a strict hierarchy. In addition, a primality witness for a unary language L, namely a word that is not in L but is in all products of languages that contain L and have an index smaller than L’s, may be of exponential length. Still, we are able to characterize compositionality by structural properties of a DFA for L, leading to a LogSpace algorithm for primality checking of unary DFAs.
Cite as

Ismaël Jecker, Orna Kupferman, and Nicolas Mazzocchi. Unary Prime Languages. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 51:1-51:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{jecker_et_al:LIPIcs.MFCS.2020.51,
  author =	{Jecker, Isma\"{e}l and Kupferman, Orna and Mazzocchi, Nicolas},
  title =	{{Unary Prime Languages}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{51:1--51:12},
  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.51},
  URN =		{urn:nbn:de:0030-drops-127177},
  doi =		{10.4230/LIPIcs.MFCS.2020.51},
  annote =	{Keywords: Deterministic Finite Automata (DFA), Regular Languages, Primality}
}
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}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.10
Coverage and Vacuity in Network Formation Games

Authors: Gili Bielous and Orna Kupferman

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
The frameworks of coverage and vacuity in formal verification analyze the effect of mutations applied to systems or their specifications. We adopt these notions to network formation games, analyzing the effect of a change in the cost of a resource. We consider two measures to be affected: the cost of the Social Optimum and extremums of costs of Nash Equilibria. Our results offer a formal framework to the effect of mutations in network formation games and include a complexity analysis of related decision problems. They also tighten the relation between algorithmic game theory and formal verification, suggesting refined definitions of coverage and vacuity for the latter.
Cite as

Gili Bielous and Orna Kupferman. Coverage and Vacuity in Network Formation Games. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 10:1-10:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bielous_et_al:LIPIcs.CSL.2020.10,
  author =	{Bielous, Gili and Kupferman, Orna},
  title =	{{Coverage and Vacuity in Network Formation Games}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{10:1--10:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.10},
  URN =		{urn:nbn:de:0030-drops-116532},
  doi =		{10.4230/LIPIcs.CSL.2020.10},
  annote =	{Keywords: Network Formation Games, Vacuity, Coverage}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2019.25
Register-Bounded Synthesis

Authors: Ayrat Khalimov and Orna Kupferman

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

Abstract
Traditional synthesis algorithms return, given a specification over finite sets of input and output Boolean variables, a finite-state transducer all whose computations satisfy the specification. Many real-life systems have an infinite state space. In particular, behaviors of systems with a finite control yet variables that range over infinite domains, are specified by automata with infinite alphabets. A register automaton has a finite set of registers, and its transitions are based on a comparison of the letters in the input with these stored in its registers. Unfortunately, reasoning about register automata is complex. In particular, the synthesis problem for specifications given by register automata, where the goal is to generate correct register transducers, is undecidable. We study the synthesis problem for systems with a bounded number of registers. Formally, the register-bounded realizability problem is to decide, given a specification register automaton A over infinite input and output alphabets and numbers k_s and k_e of registers, whether there is a system transducer T with at most k_s registers such that for all environment transducers T' with at most k_e registers, the computation T|T', generated by the interaction of T with T', satisfies the specification A. The register-bounded synthesis problem is to construct such a transducer T, if exists. The bounded setting captures better real-life scenarios where bounds on the systems and/or its environment are known. In addition, the bounds are the key to new synthesis algorithms, and, as recently shown in [A. Khalimov et al., 2018], they lead to decidability. Our contributions include a stronger specification formalism (universal register parity automata), simpler algorithms, which enable a clean complexity analysis, a study of settings in which both the system and the environment are bounded, and a study of the theoretical aspects of the setting; in particular, the differences among a fixed, finite, and infinite number of registers, and the determinacy of the corresponding games.
Cite as

Ayrat Khalimov and Orna Kupferman. Register-Bounded Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{khalimov_et_al:LIPIcs.CONCUR.2019.25,
  author =	{Khalimov, Ayrat and Kupferman, Orna},
  title =	{{Register-Bounded Synthesis}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{25:1--25: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.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.25},
  URN =		{urn:nbn:de:0030-drops-109277},
  doi =		{10.4230/LIPIcs.CONCUR.2019.25},
  annote =	{Keywords: Synthesis, Register Automata, Register Transducers}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2019.100
Minimizing GFG Transition-Based Automata (Track B: Automata, Logic, Semantics, and Theory of Programming)

Authors: Bader Abu Radi and Orna Kupferman

Published in: LIPIcs, Volume 132, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)

Abstract
While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games automata. The latter are nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. The minimization problem for nondeterministic and deterministic Büchi and co-Büchi word automata are PSPACE-complete and NP-complete, respectively. We describe a polynomial minimization algorithm for good-for-games co-Büchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set of designated transitions only finitely often. Our algorithm is based on a sequence of transformations we apply to the automaton, on top of which a minimal quotient automaton is defined.
Cite as

Bader Abu Radi and Orna Kupferman. Minimizing GFG Transition-Based Automata (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 100:1-100:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{aburadi_et_al:LIPIcs.ICALP.2019.100,
  author =	{Abu Radi, Bader and Kupferman, Orna},
  title =	{{Minimizing GFG Transition-Based Automata}},
  booktitle =	{46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)},
  pages =	{100:1--100:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-109-2},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{132},
  editor =	{Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.100},
  URN =		{urn:nbn:de:0030-drops-106761},
  doi =		{10.4230/LIPIcs.ICALP.2019.100},
  annote =	{Keywords: Minimization, Deterministic co-B\"{u}chi Automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.23
Timed Network Games with Clocks

Authors: Guy Avni, Shibashis Guha, and Orna Kupferman

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertices. The cost of traversing an edge depends on the load; namely, number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in determining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, actual sharing and congestion of resources crucially depends on time. In [G. Avni et al., 2017], we introduced timed network games, which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. Each edge in the network is guarded by the time intervals in which it can be traversed, which forces the players to spend time in the vertices. In this work we significantly extend the way time can be referred to in timed network games. In the model we study, the network is equipped with clocks, and, as in timed automata, edges are guarded by constraints on the values of the clocks, and their traversal may involve a reset of some clocks. We argue that the stronger model captures many realistic networks. The addition of clocks breaks the techniques we developed in [G. Avni et al., 2017] and we develop new techniques in order to show that positive results on classic network games carry over to the stronger timed setting.
Cite as

Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games with Clocks. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2018.23,
  author =	{Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =	{{Timed Network Games with Clocks}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul 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.MFCS.2018.23},
  URN =		{urn:nbn:de:0030-drops-96053},
  doi =		{10.4230/LIPIcs.MFCS.2018.23},
  annote =	{Keywords: Network games, Timed automata, Nash equilibrium, Equilibrium inefficiency}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2018.35
Spanning-Tree Games

Authors: Dan Hefetz, Orna Kupferman, Amir Lellouche, and Gal Vardi

Published in: LIPIcs, Volume 117, 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)

Abstract
We introduce and study a game variant of the classical spanning-tree problem. Our spanning-tree game is played between two players, min and max, who alternate turns in jointly constructing a spanning tree of a given connected weighted graph G. Starting with the empty graph, in each turn a player chooses an edge that does not close a cycle in the forest that has been generated so far and adds it to that forest. The game ends when the chosen edges form a spanning tree in G. The goal of min is to minimize the weight of the resulting spanning tree and the goal of max is to maximize it. A strategy for a player is a function that maps each forest in G to an edge that is not yet in the forest and does not close a cycle. We show that while in the classical setting a greedy approach is optimal, the game setting is more complicated: greedy strategies, namely ones that choose in each turn the lightest (min) or heaviest (max) legal edge, are not necessarily optimal, and calculating their values is NP-hard. We study the approximation ratio of greedy strategies. We show that while a greedy strategy for min guarantees nothing, the performance of a greedy strategy for max is satisfactory: it guarantees that the weight of the generated spanning tree is at least w(MST(G))/2, where w(MST(G)) is the weight of a maximum spanning tree in G, and its approximation ratio with respect to an optimal strategy for max is 1.5+1/w(MST(G)), assuming weights in [0,1]. We also show that these bounds are tight. Moreover, in a stochastic setting, where weights for the complete graph K_n are chosen at random from [0,1], the expected performance of greedy strategies is asymptotically optimal. Finally, we study some variants of the game and study an extension of our results to games on general matroids.
Cite as

Dan Hefetz, Orna Kupferman, Amir Lellouche, and Gal Vardi. Spanning-Tree Games. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{hefetz_et_al:LIPIcs.MFCS.2018.35,
  author =	{Hefetz, Dan and Kupferman, Orna and Lellouche, Amir and Vardi, Gal},
  title =	{{Spanning-Tree Games}},
  booktitle =	{43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-086-6},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{117},
  editor =	{Potapov, Igor and Spirakis, Paul 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.MFCS.2018.35},
  URN =		{urn:nbn:de:0030-drops-96171},
  doi =		{10.4230/LIPIcs.MFCS.2018.35},
  annote =	{Keywords: Algorithms, Games, Minimum/maximum spanning tree, Greedy algorithms}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2018.157
The Unfortunate-Flow Problem

Authors: Orna Kupferman and Gal Vardi

Published in: LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)

Abstract
In the traditional maximum-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow into outgoing edges. The problem is one of the most fundamental problems in TCS, with application in numerous domains. The fact a maximal-flow algorithm directs the flow in all the vertices of the network corresponds to a setting in which the authority has control in all vertices. Many applications in which the maximal-flow problem is applied involve an adversarial setting, where the authority does not have such a control. We introduce and study the unfortunate flow problem, which studies the flow that is guaranteed to reach the target when the edges that leave the source are saturated, yet the most unfortunate decisions are taken in the vertices. When the incoming flow to a vertex is greater than the outgoing capacity, flow is lost. The problem models evacuation scenarios where traffic is stuck due to jams in junctions and communication networks where packets are dropped in overloaded routers. We study the theoretical properties of unfortunate flows, show that the unfortunate-flow problem is co-NP-complete and point to polynomial fragments. We introduce and study interesting variants of the problem: integral unfortunate flow, where the flow along edges must be integral, controlled unfortunate flow, where the edges from the source need not be saturated and may be controlled, and no-loss controlled unfortunate flow, where the controlled flow must not be lost.
Cite as

Orna Kupferman and Gal Vardi. The Unfortunate-Flow Problem. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 157:1-157:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.ICALP.2018.157,
  author =	{Kupferman, Orna and Vardi, Gal},
  title =	{{The Unfortunate-Flow Problem}},
  booktitle =	{45th International Colloquium on Automata, Languages, and Programming (ICALP 2018)},
  pages =	{157:1--157:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-076-7},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{107},
  editor =	{Chatzigiannakis, Ioannis and Kaklamanis, Christos and Marx, D\'{a}niel and Sannella, Donald},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.157},
  URN =		{urn:nbn:de:0030-drops-91613},
  doi =		{10.4230/LIPIcs.ICALP.2018.157},
  annote =	{Keywords: Flow Network, Graph Algorithms, Games}
}
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.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.FSTTCS.2017.38
Flow Games

Authors: Orna Kupferman, Gal Vardi, and Moshe Y. Vardi

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

Abstract
In the traditional maximal-flow problem, the goal is to transfer maximum flow in a network by directing, in each vertex in the network, incoming flow into outgoing edges. While the problem has been extensively used in order to optimize the performance of networks in numerous application areas, it corresponds to a setting in which the authority has control on all vertices of the network. Today's computing environment involves parties that should be considered adversarial. We introduce and study {\em flow games}, which capture settings in which the authority can control only part of the vertices. In these games, the vertices are partitioned between two players: the authority and the environment. While the authority aims at maximizing the flow, the environment need not cooperate. We argue that flow games capture many modern settings, such as partially-controlled pipe or road systems or hybrid software-defined communication networks. We show that the problem of finding the maximal flow as well as an optimal strategy for the authority in an acyclic flow game is $\Sigma_2^P$-complete, and is already $\Sigma_2^P$-hard to approximate. We study variants of the game: a restriction to strategies that ensure no loss of flow, an extension to strategies that allow non-integral flows, which we prove to be stronger, and a dynamic setting in which a strategy for a vertex is chosen only once flow reaches the vertex. We discuss additional variants and their applications, and point to several interesting open problems.
Cite as

Orna Kupferman, Gal Vardi, and Moshe Y. Vardi. Flow Games. 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. 38:1-38:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2017.38,
  author =	{Kupferman, Orna and Vardi, Gal and Vardi, Moshe Y.},
  title =	{{Flow Games}},
  booktitle =	{37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017)},
  pages =	{38:1--38:16},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2017.38},
  URN =		{urn:nbn:de:0030-drops-83738},
  doi =		{10.4230/LIPIcs.FSTTCS.2017.38},
  annote =	{Keywords: Flow networks, Two-player Games, Algorithms}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2017.37
Timed Network Games

Authors: Guy Avni, Shibashis Guha, and Orna Kupferman

Published in: LIPIcs, Volume 83, 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)

Abstract
Network games are widely used as a model for selfish resource-allocation problems. In the classical model, each player selects a path connecting her source and target vertex. The cost of traversing an edge depends on the number of players that traverse it. Thus, it abstracts the fact that different users may use a resource at different times and for different durations, which plays an important role in defining the costs of the users in reality. For example, when transmitting packets in a communication network, routing traffic in a road network, or processing a task in a production system, the traversal of the network involves an inherent delay, and so sharing and congestion of resources crucially depends on time. We study timed network games, which add a time component to network games. Each vertex v in the network is associated with a cost function, mapping the load on v to the price that a player pays for staying in v for one time unit with this load. In addition, each edge has a guard, describing time intervals in which the edge can be traversed, forcing the players to spend time on vertices. Unlike earlier work that add a time component to network games, the time in our model is continuous and cannot be discretized. In particular, players have uncountably many strategies, and a game may have uncountably many pure Nash equilibria. We study properties of timed network games with cost-sharing or congestion cost functions: their stability, equilibrium inefficiency, and complexity. In particular, we show that the answer to the question whether we can restrict attention to boundary strategies, namely ones in which edges are traversed only at the boundaries of guards, is mixed.
Cite as

Guy Avni, Shibashis Guha, and Orna Kupferman. Timed Network Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 37:1-37:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.MFCS.2017.37,
  author =	{Avni, Guy and Guha, Shibashis and Kupferman, Orna},
  title =	{{Timed Network Games}},
  booktitle =	{42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017)},
  pages =	{37:1--37:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-046-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{83},
  editor =	{Larsen, Kim G. and Bodlaender, Hans L. and Raskin, Jean-Francois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2017.37},
  URN =		{urn:nbn:de:0030-drops-80675},
  doi =		{10.4230/LIPIcs.MFCS.2017.37},
  annote =	{Keywords: Network Games, Timed Automata, Nash Equilibrium, Equilibrium Inefficiency}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.9
Flow Logic

Authors: Orna Kupferman and Gal Vardi

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

Abstract
A flow network is a directed graph in which each edge has a capacity, bounding the amount of flow that can travel through it. Flow networks have attracted a lot of research in computer science. Indeed, many questions in numerous application areas can be reduced to questions about flow networks. This includes direct applications, namely a search for a maximal flow in networks, as well as less direct applications, like maximal matching or optimal scheduling. Many of these applications would benefit from a framework in which one can formally reason about properties of flow networks that go beyond their maximal flow. We introduce Flow Logics: modal logics that treat flow functions as explicit first-order objects and enable the specification of rich properties of flow networks. The syntax of our logic BFL* (Branching Flow Logic) is similar to the syntax of the temporal logic CTL*, except that atomic assertions may be flow propositions, like > \gamma or \geq \gamma, for \gamma \in \N, which refer to the value of the flow in a vertex, and that first-order quantification can be applied both to paths and to flow functions. For example, the BFL* formula \Ef ((\geq 100) \wedge AG({\it low} \rightarrow (\leq 20)) states that there is a legal flow function in which the flow is above 100 and in all paths, the amount of flow that travels through vertices with low security is at most 20. We present an exhaustive study of the theoretical and practical aspects of BFL*, as well as extensions and fragments of it. Our extensions include flow quantifications that range over non-integral flow functions or over maximal flow functions, path quantification that ranges over paths along which non-zero flow travels, past operators, and first-order quantification of flow values. We focus on the model-checking problem and show that it is PSPACE-complete, as it is for CTL*. Handling of flow quantifiers, however, increases the complexity in terms of the network to P^{NP}, even for the LFL and BFL fragments, which are the flow-counterparts of LTL and CTL. We are still able to point to a useful fragment of BFL* for which the model-checking problem can be solved in polynomial time.
Cite as

Orna Kupferman and Gal Vardi. Flow Logic. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 9:1-9:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.CONCUR.2017.9,
  author =	{Kupferman, Orna and Vardi, Gal},
  title =	{{Flow Logic}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{9:1--9:18},
  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.9},
  URN =		{urn:nbn:de:0030-drops-77796},
  doi =		{10.4230/LIPIcs.CONCUR.2017.9},
  annote =	{Keywords: Flow Network, Temporal Logic}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.28
High-Quality Synthesis Against Stochastic Environments

Authors: Shaull Almagor and Orna Kupferman

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
In the classical synthesis problem, we are given a linear temporal logic (LTL) formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi: with every sequence of input signals, the transducer associates a sequence of output signals so that the generated computation satisfies psi. One weakness of automated synthesis in practice is that it pays no attention to the quality of the synthesized system. Indeed, the classical setting is Boolean: a computation satisfies a specification or does not satisfy it. Accordingly, while the synthesized system is correct, there is no guarantee about its quality. In recent years, researchers have considered extensions of the classical Boolean setting to a quantitative one. The logic FLTL is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an FLTL formula is a real value in [0,1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Decision problems for LTL become search or optimization problems for FLTL. In particular, in the synthesis problem, the goal is to generate a transducer that satisfies the specification in the highest possible quality. Previous work considered the worst-case setting, where the goal is to maximize the quality of the computation with the minimal quality. We introduce and solve the stochastic setting, where the goal is to generate a transducer that maximizes the expected quality of a computation, subject to a given distribution of the input signals. Thus, rather than being hostile, the environment is assumed to be probabilistic, which corresponds to many realistic settings. We show that the problem is 2EXPTIME-complete, like classical LTL synthesis. The complexity stays 2EXPTIME also in two extensions we consider: one that maximizes the expected quality while guaranteeing that the minimal quality is, with probability 1, above a given threshold, and one that allows assumptions on the environment.
Cite as

Shaull Almagor and Orna Kupferman. High-Quality Synthesis Against Stochastic Environments. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 28:1-28:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CSL.2016.28,
  author =	{Almagor, Shaull and Kupferman, Orna},
  title =	{{High-Quality Synthesis Against Stochastic Environments}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{28:1--28:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.28},
  URN =		{urn:nbn:de:0030-drops-65688},
  doi =		{10.4230/LIPIcs.CSL.2016.28},
  annote =	{Keywords: Stochastic and Quantitative Synthesis, Markov Decision Process}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2016.9
Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

Authors: Shaull Almagor, Orna Kupferman, and Yaron Velner

Published in: LIPIcs, Volume 59, 27th International Conference on Concurrency Theory (CONCUR 2016)

Abstract
In Boolean synthesis, we are given an LTL specification, and the goal is to construct a transducer that realizes it against an adversarial environment. Often, a specification contains both Boolean requirements that should be satisfied against an adversarial environment, and multi-valued components that refer to the quality of the satisfaction and whose expected cost we would like to minimize with respect to a probabilistic environment. In this work we study, for the first time, mean-payoff games in which the system aims at minimizing the expected cost against a probabilistic environment, while surely satisfying an omega-regular condition against an adversarial environment. We consider the case the omega-regular condition is given as a parity objective or by an LTL formula. We show that in general, optimal strategies need not exist, and moreover, the limit value cannot be approximated by finite-memory strategies. We thus focus on computing the limit-value, and give tight complexity bounds for synthesizing epsilon-optimal strategies for both finite-memory and infinite-memory strategies. We show that our game naturally arises in various contexts of synthesis with Boolean and multi-valued objectives. Beyond direct applications, in synthesis with costs and rewards to certain behaviors, it allows us to compute the minimal sensing cost of omega-regular specifications -- a measure of quality in which we look for a transducer that minimizes the expected number of signals that are read from the input.
Cite as

Shaull Almagor, Orna Kupferman, and Yaron Velner. Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2016.9,
  author =	{Almagor, Shaull and Kupferman, Orna and Velner, Yaron},
  title =	{{Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis}},
  booktitle =	{27th International Conference on Concurrency Theory (CONCUR 2016)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-017-0},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{59},
  editor =	{Desharnais, Jos\'{e}e and Jagadeesan, Radha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2016.9},
  URN =		{urn:nbn:de:0030-drops-61689},
  doi =		{10.4230/LIPIcs.CONCUR.2016.9},
  annote =	{Keywords: Stochastic and Quantitative Synthesis, Mean Payoff Games, Sensing.}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2016.62
Eulerian Paths with Regular Constraints

Authors: Orna Kupferman and Gal Vardi

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

Abstract
Labeled graphs, in which edges are labeled by letters from some alphabet Sigma, are extensively used to model many types of relations associated with actions, costs, owners, or other properties. Each path in a labeled graph induces a word in Sigma^* -- the one obtained by concatenating the letters along the edges in the path. Classical graph-theory problems give rise to new problems that take these words into account. We introduce and study the constrained Eulerian path problem. The input to the problem is a Sigma-labeled graph G and a specification L \subseteq Sigma^*. The goal is to find an Eulerian path in G that satisfies L. We consider several classes of the problem, defined by the classes of G and L. We focus on the case L is regular and show that while the problem is in general NP-complete, even for very simple graphs and specifications, there are classes that can be solved efficiently. Our results extend work on Eulerian paths with edge-order constraints. We also study the constrained Chinese postman problem, where edges have costs and the goal is to find a cheapest path that contains each edge at least once and satisfies the specification. Finally, we define and study the Eulerian language of a graph, namely the set of words along its Eulerian paths.
Cite as

Orna Kupferman and Gal Vardi. Eulerian Paths with Regular Constraints. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 58, pp. 62:1-62:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.MFCS.2016.62,
  author =	{Kupferman, Orna and Vardi, Gal},
  title =	{{Eulerian Paths with Regular Constraints}},
  booktitle =	{41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016)},
  pages =	{62:1--62: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.62},
  URN =		{urn:nbn:de:0030-drops-64747},
  doi =		{10.4230/LIPIcs.MFCS.2016.62},
  annote =	{Keywords: Eulerian paths, regular languages}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.365
Congestion Games with Multisets of Resources and Applications in Synthesis

Authors: Guy Avni, Orna Kupferman, and Tami Tamir

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
In classical congestion games, players' strategies are subsets of resources. We introduce and study multiset congestion games, where players' strategies are multisets of resources. Thus, in each strategy a player may need to use each resource a different number of times, and his cost for using the resource depends on the load that he and the other players generate on the resource. Beyond the theoretical interest in examining the effect of a repeated use of resources, our study enables better understanding of non-cooperative systems and environments whose behavior is not covered by previously studied models. Indeed, congestion games with multiset-strategies arise, for example, in production planing and network formation with tasks that are more involved than reachability. We study in detail the application of synthesis from component libraries: different users synthesize systems by gluing together components from a component library. A component may be used in several systems and may be used several times in a system. The performance of a component and hence the system's quality depends on the load on it. Our results reveal how the richer setting of multisets congestion games affects the stability and equilibrium efficiency compared to standard congestion games. In particular, while we present very simple instances with no pure Nash equilibrium and prove tighter and simpler lower bounds for equilibrium inefficiency, we are also able to show that some of the positive results known for affine and weighted congestion games apply to the richer setting of multisets.
Cite as

Guy Avni, Orna Kupferman, and Tami Tamir. Congestion Games with Multisets of Resources and Applications in Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 365-379, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{avni_et_al:LIPIcs.FSTTCS.2015.365,
  author =	{Avni, Guy and Kupferman, Orna and Tamir, Tami},
  title =	{{Congestion Games with Multisets of Resources and Applications in Synthesis}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{365--379},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.365},
  URN =		{urn:nbn:de:0030-drops-56358},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.365},
  annote =	{Keywords: Congestion games, Multiset strategies, Equilibrium existence and computation, Equilibrium inefficiency}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2015.380
The Sensing Cost of Monitoring and Synthesis

Authors: Shaull Almagor, Denis Kuperberg, and Orna Kupferman

Published in: LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)

Abstract
In FSTTCS 2014, we introduced sensing as a new complexity measure for the complexity of regular languages. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read by a deterministic automaton in order to decide its membership in the language. In this paper, we consider sensing in two principal applications of deterministic automata. The first is monitoring: we are given a computation in an on-line manner, and we have to decide whether it satisfies the specification. The second is synthesis: we are given a sequence of inputs in an on-line manner and we have to generate a sequence of outputs so that the resulting computation satisfies the specification. In the first, our goal is to design a monitor that handles all computations and minimizes the expected average number of sensors used in the monitoring process. In the second, our goal is to design a transducer that realizes the specification for all input sequences and minimizes the expected average number of sensors used for reading the inputs. We argue that the two applications require new and different frameworks for reasoning about sensing, and develop such frameworks. We focus on safety languages. We show that for monitoring, minimal sensing is attained by a monitor based on the minimal deterministic automaton for the language. For synthesis, however, the setting is more challenging: minimizing the sensing may require exponentially bigger transducers, and the problem of synthesizing a minimally-sensing transducer is EXPTIME-complete even for safety specifications given by deterministic automata.
Cite as

Shaull Almagor, Denis Kuperberg, and Orna Kupferman. The Sensing Cost of Monitoring and Synthesis. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 380-393, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2015.380,
  author =	{Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
  title =	{{The Sensing Cost of Monitoring and Synthesis}},
  booktitle =	{35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015)},
  pages =	{380--393},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-97-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{45},
  editor =	{Harsha, Prahladh and Ramalingam, G.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.380},
  URN =		{urn:nbn:de:0030-drops-56563},
  doi =		{10.4230/LIPIcs.FSTTCS.2015.380},
  annote =	{Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2015.175
On Relative and Probabilistic Finite Counterability

Authors: Orna Kupferman and Gal Vardi

Published in: LIPIcs, Volume 41, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015)

Abstract
A counterexample to the satisfaction of a linear property psi in a system S is an infinite computation of S that violates psi. Counterexamples are of great help in detecting design errors and in modeling methodologies such as CEGAR. When psi is a safety property, a counterexample to its satisfaction need not be infinite. Rather, it is a bad-prefix for psi: a finite word all whose extensions violate psi. The existence of finite counterexamples is very helpful in practice. Liveness properties do not have bad-prefixes and thus do not have finite counterexamples. We extend the notion of finite counterexamples to non-safety properties. We study counterable languages - ones that have at least one bad-prefix. Thus, a language is counterable iff it is not liveness. Three natural problems arise: (1) Given a language, decide whether it is counterable, (2) study the length of minimal bad-prefixes for counterable languages, and (3) develop algorithms for detecting bad-prefixes for counterable languages. We solve the problems for languages given by means of LTL formulas or nondeterministic Büchi automata. In particular, our EXPSPACE-completeness proof for the problem of deciding whether a given LTL formula is counterable, and hence also for deciding whether it is liveness, settles a long-standing open problem. We also make finite counterexamples more relevant and helpful by introducing two variants of the traditional definition of bad-prefixes. The first adds a probabilistic component to the definition. There, a prefix is bad if almost all its extensions violate the property. The second makes it relative to the system. There, a prefix is bad if all its extensions in the system violate the property. We also study the combination of the probabilistic and relative variants. Our framework suggests new variants also of safety and liveness languages. We solve the above three problems for the different variants. Interestingly, the probabilistic variant not only increases the chances to return finite counterexamples, but also makes the solution of the three problems exponentially easier.
Cite as

Orna Kupferman and Gal Vardi. On Relative and Probabilistic Finite Counterability. In 24th EACSL Annual Conference on Computer Science Logic (CSL 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 41, pp. 175-192, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.CSL.2015.175,
  author =	{Kupferman, Orna and Vardi, Gal},
  title =	{{On Relative and Probabilistic Finite Counterability}},
  booktitle =	{24th EACSL Annual Conference on Computer Science Logic (CSL 2015)},
  pages =	{175--192},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-90-3},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{41},
  editor =	{Kreutzer, Stephan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2015.175},
  URN =		{urn:nbn:de:0030-drops-54147},
  doi =		{10.4230/LIPIcs.CSL.2015.175},
  annote =	{Keywords: Model Checking, Counterexamples, Safety, Liveness, Probability, omega-Regular Languages}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2015.325
Repairing Multi-Player Games

Authors: Shaull Almagor, Guy Avni, and Orna Kupferman

Published in: LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015)

Abstract
Synthesis is the automated construction of systems from their specifications. Modern systems often consist of interacting components, each having its own objective. The interaction among the components is modeled by a multi-player game. Strategies of the components induce a trace in the game, and the objective of each component is to force the game into a trace that satisfies its specification. This is modeled by augmenting the game with omega-regular winning conditions. Unlike traditional synthesis games, which are zero-sum, here the objectives of the components do not necessarily contradict each other. Accordingly, typical questions about these games concern their stability - whether the players reach an equilibrium, and their social welfare - maximizing the set of (possibly weighted) specifications that are satisfied. We introduce and study repair of multi-player games. Given a game, we study the possibility of modifying the objectives of the players in order to obtain stability or to improve the social welfare. Specifically, we solve the problem of modifying the winning conditions in a given concurrent multi-player game in a way that guarantees the existence of a Nash equilibrium. Each modification has a value, reflecting both the cost of strengthening or weakening the underlying specifications, as well as the benefit of satisfying specifications in the obtained equilibrium. We seek optimal modifications, and we study the problem for various omega-regular objectives and various cost and benefit functions. We analyze the complexity of the problem in the general setting as well as in one with a fixed number of players. We also study two additional types of repair, namely redirection of transitions and control of a subset of the players.
Cite as

Shaull Almagor, Guy Avni, and Orna Kupferman. Repairing Multi-Player Games. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 325-339, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.CONCUR.2015.325,
  author =	{Almagor, Shaull and Avni, Guy and Kupferman, Orna},
  title =	{{Repairing Multi-Player Games}},
  booktitle =	{26th International Conference on Concurrency Theory (CONCUR 2015)},
  pages =	{325--339},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-91-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{42},
  editor =	{Aceto, Luca and de Frutos Escrig, David},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.325},
  URN =		{urn:nbn:de:0030-drops-53741},
  doi =		{10.4230/LIPIcs.CONCUR.2015.325},
  annote =	{Keywords: Nash equilibrium, concurrent games, repair}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2014.33
Properties and Utilization of Capacitated Automata (Invited Talk)

Authors: Orna Kupferman and Tami Tamir

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We study capacitated automata(CAs), where transitions correspond to resources and may have bounded capacities. Each transition in a CA is associated with a (possibly infinite) bound on the number of times it may be traversed. We study CAs from two points of view. The first is that of traditional automata theory, where we view CAs as recognizers of formal languages and examine their expressive power, succinctness, and determinization. The second is that of resource-allocation theory, where we view CAs as a rich description of a flow network and study their utilization.
Cite as

Orna Kupferman and Tami Tamir. Properties and Utilization of Capacitated Automata (Invited Talk). In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 33-44, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.FSTTCS.2014.33,
  author =	{Kupferman, Orna and Tamir, Tami},
  title =	{{Properties and Utilization of Capacitated Automata}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{33--44},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.33},
  URN =		{urn:nbn:de:0030-drops-48306},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.33},
  annote =	{Keywords: Automata, Capacitated transitions, Determinization, Maximum utilization}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.161
Regular Sensing

Authors: Shaull Almagor, Denis Kuperberg, and Orna Kupferman

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
The size of deterministic automata required for recognizing regular and omega-regular languages is a well-studied measure for the complexity of languages. We introduce and study a new complexity measure, based on the sensing required for recognizing the language. Intuitively, the sensing cost quantifies the detail in which a random input word has to be read in order to decide its membership in the language. We show that for finite words, size and sensing are related, and minimal sensing is attained by minimal automata. Thus, a unique minimal-sensing deterministic automaton exists, and is based on the language's right-congruence relation. For infinite words, the minimal sensing may be attained only by an infinite sequence of automata. We show that the optimal limit cost of such sequences can be characterized by the language's right-congruence relation, which enables us to find the sensing cost of omega-regular languages in polynomial time.
Cite as

Shaull Almagor, Denis Kuperberg, and Orna Kupferman. Regular Sensing. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 161-173, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{almagor_et_al:LIPIcs.FSTTCS.2014.161,
  author =	{Almagor, Shaull and Kuperberg, Denis and Kupferman, Orna},
  title =	{{Regular Sensing}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{161--173},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.161},
  URN =		{urn:nbn:de:0030-drops-48409},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.161},
  annote =	{Keywords: Automata, regular languages, omega-regular languages, complexity, sensing, minimization}
}
Document
DOI: 10.4230/LIPIcs.CSL.2011.248
Unifying Büchi Complementation Constructions

Authors: Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke

Published in: LIPIcs, Volume 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL (2011)

Abstract
Complementation of Buechi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of Kahler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves Schewe's tight bound.
Cite as

Seth Fogarty, Orna Kupferman, Moshe Y. Vardi, and Thomas Wilke. Unifying Büchi Complementation Constructions. In Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 12, pp. 248-263, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{fogarty_et_al:LIPIcs.CSL.2011.248,
  author =	{Fogarty, Seth and Kupferman, Orna and Vardi, Moshe Y. and Wilke, Thomas},
  title =	{{Unifying B\"{u}chi Complementation Constructions}},
  booktitle =	{Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL},
  pages =	{248--263},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-32-3},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{12},
  editor =	{Bezem, Marc},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2011.248},
  URN =		{urn:nbn:de:0030-drops-32357},
  doi =		{10.4230/LIPIcs.CSL.2011.248},
  annote =	{Keywords: B\"{u}chi automata, complementation, ranks, determinism in the limit}
}
Document
DOI: 10.4230/LIPIcs.STACS.2011.615
Temporal Synthesis for Bounded Systems and Environments

Authors: Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis

Published in: LIPIcs, Volume 9, 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)

Abstract
Temporal synthesis is the automated construction of a system from its temporal specification. It is by now realized that requiring the synthesized system to satisfy the specifications against all possible environments may be too demanding, and, dually, allowing all systems may be not demanding enough. In this work we study bounded temporal synthesis, in which bounds on the sizes of the state space of the system and the environment are additional parameters to the synthesis problem. This study is motivated by the fact that such bounds may indeed change the answer to the synthesis problem, as well as the theoretical and computational aspects of the synthesis problem. In particular, a finer analysis of synthesis, which takes system and environment sizes into account, yields deeper insight into the quantificational structure of the synthesis problem and the relationship between strong synthesis -- there exists a system such that for all environments, the specification holds, and weak synthesis -- for all environments there exists a system such that the specification holds. We first show that unlike the unbounded setting, where determinacy of regular games implies that strong and weak synthesis coincide, these notions do not coincide in the bounded setting. We then turn to study the complexity of deciding strong and weak synthesis. We show that bounding the size of the system or both the system and the environment, turns the synthesis problem into a search problem, and one cannot expect to do better than brute-force search. In particular, the synthesis problem for bounded systems and environment is Sigma^P_2-complete (in terms of the bounds, for a specification given by a deterministic automaton). We also show that while bounding the environment may lead to the synthesis of specifications that are otherwise unrealizable, such relaxation of the problem comes at a high price from a complexity-theoretic point of view.
Cite as

Orna Kupferman, Yoad Lustig, Moshe Y. Vardi, and Mihalis Yannakakis. Temporal Synthesis for Bounded Systems and Environments. In 28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011). Leibniz International Proceedings in Informatics (LIPIcs), Volume 9, pp. 615-626, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kupferman_et_al:LIPIcs.STACS.2011.615,
  author =	{Kupferman, Orna and Lustig, Yoad and Vardi, Moshe Y. and Yannakakis, Mihalis},
  title =	{{Temporal Synthesis for Bounded Systems and Environments}},
  booktitle =	{28th International Symposium on Theoretical Aspects of Computer Science (STACS 2011)},
  pages =	{615--626},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-25-5},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{9},
  editor =	{Schwentick, Thomas and D\"{u}rr, Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2011.615},
  URN =		{urn:nbn:de:0030-drops-30481},
  doi =		{10.4230/LIPIcs.STACS.2011.615},
  annote =	{Keywords: temporal synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.412
Parityizing Rabin and Streett

Authors: Udi Boker, Orna Kupferman, and Avital Steinitz

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

Abstract
The parity acceptance condition for $omega$-regular languages is a special case of the Rabin and Streett acceptance conditions. While the parity acceptance condition is as expressive as the richer conditions, in both the deterministic and nondeterministic settings, Rabin and Streett automata are more succinct, and their translation to parity automata may blow-up the state space. The appealing properties of the parity condition, mainly the fact it is dualizable and allows for memoryless strategies, make such a translation useful in various decision procedures. In this paper we study languages that are recognizable by an automaton on top of which one can define both a Rabin and a Streett condition for the language. We show that if the underlying automaton is deterministic, then we can define on top of it also a parity condition for the language. We also show that this relation does not hold in the nondeterministic setting. Finally, we use the construction of the parity condition in the deterministic case in order to solve the problem of deciding whether a given Rabin or Streett automaton has an equivalent parity automaton on the same structure, and show that it is PTIME-complete in the deterministic setting and is PSPACE-complete in the nondeterministic setting.
Cite as

Udi Boker, Orna Kupferman, and Avital Steinitz. Parityizing Rabin and Streett. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 412-423, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{boker_et_al:LIPIcs.FSTTCS.2010.412,
  author =	{Boker, Udi and Kupferman, Orna and Steinitz, Avital},
  title =	{{Parityizing Rabin and Streett}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{412--423},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.412},
  URN =		{urn:nbn:de:0030-drops-28822},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.412},
  annote =	{Keywords: omega-automata, Rabin condition, Streett condition, parity condition}
}
Document
DOI: 10.4230/DagSemProc.09501.1
09501 Abstracts Collection – Software Synthesis

Authors: Ratislav Bodik, Orna Kupferman, Dougla R. Smith, and Eran Yahav

Published in: Dagstuhl Seminar Proceedings, Volume 9501, Software Synthesis (2010)

Abstract
From 06.12.09 to 11.12.09, the Dagstuhl Seminar 09501 ``Software Synthesis '' in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Ratislav Bodik, Orna Kupferman, Dougla R. Smith, and Eran Yahav. 09501 Abstracts Collection – Software Synthesis. In Software Synthesis. Dagstuhl Seminar Proceedings, Volume 9501, pp. 1-15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{bodik_et_al:DagSemProc.09501.1,
  author =	{Bodik, Ratislav and Kupferman, Orna and Smith, Dougla R. and Yahav, Eran},
  title =	{{09501 Abstracts Collection – Software Synthesis}},
  booktitle =	{Software Synthesis},
  pages =	{1--15},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9501},
  editor =	{Ratislav Bodik and Orna Kupferman and Douglas R. Smith and Eran Yahav},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09501.1},
  URN =		{urn:nbn:de:0030-drops-26696},
  doi =		{10.4230/DagSemProc.09501.1},
  annote =	{Keywords: Software Synthesis, Verification, Theorem Proving, Program Analysis, Programming by Demonstration}
}
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