Orna Kupferman

Search for another author

Author Description

Ask a Question About This Mathematician

All published works (35)

Variable automata over infinite alphabets

2025-05-20

Orna Grümberg , Orna Kupferman , Sarai Sheinvald

Synthesis with Guided Environments

2025-01-01

Orna Kupferman , Ofer Leshkowitz

Non-Zero-Sum Games with Multiple Weighted Objectives

2025-01-01

Yoav Feinstein , Orna Kupferman , Noam Shenwald

Synthesis with Privacy Against an Observer

2024-11-13

Orna Kupferman , Ofer Leshkowitz , Namma Shamash Halevy

We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets $I$ and … We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets $I$ and $O$ of input and output signals. The input to the synthesis problem contains, in addition to a specification, also a list of secrets, a function $cost: I\cup O\rightarrow\mathbb{N}$, which maps each signal to the cost of hiding it, and a bound $b\in\mathbb{N}$ on the budget that the system may use for hiding of signals. The desired output is an $(I/O)$-transducer $T$ and a set $H\subseteq I\cup O$ of signals that respects the bound on the budget, thus $\sum_{s\in H} cost(s)\leq b$, such that for every possible interaction of $T$, the generated computation satisfies the specification, yet an observer, from whom the signals in $H$ are hidden, cannot evaluate the secrets. We first show that the problem's complexity is 2EXPTIME-complete for specifications and secrets in LTL, making it no harder than synthesis without privacy requirements. We then analyze the complexity further, isolating the two aspects that do not exist in traditional synthesis: the need to hide secret values and the need to choose the set $H$. We do this by studying settings in which traditional synthesis is solvable in polynomial time -- when the specification formalism is deterministic automata and when the system is closed -- and show that each of these aspects adds an exponential blow-up in complexity. We continue and study bounded synthesis with privacy, where the input includes a bound on the synthesized transducer size, as well as a variant of the problem in which the observer has knowledge, either about the specification or about the system, which can be helpful in evaluating the secrets. Additionally, we study certified privacy, where the synthesis algorithm provides certification that the secrets remain hidden.

Chat View PDF

On Semantically-Deterministic Automata

2023-01-01

Bader Abu Radi , Orna Kupferman

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, … 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 deterministic automata in formal methods can actually 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\"uchi, co-B\"uchi, 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\"uchi and co-B\"uchi 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.

Chat View PDF

Minimization and Canonization of GFG Transition-Based Automata

2022-08-02

Bader Abu Radi , Orna Kupferman

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) automata. The latter are nondeterministic automata that can … While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) 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 deterministic B\"uchi and co-B\"uchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG co-B\"uchi word automata with transition-based acceptance. Thus, a run is accepting if it traverses a set $\alpha$ 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. We use our minimization algorithm to show canonicity for transition-based GFG co-B\"uchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in $\alpha$) and once we saturate the automata with $\alpha$-transitions, we get full isomorphism.

Chat View PDF

Certifying DFA Bounds for Recognition and Separation

2022-03-15

Orna Kupferman , Nir Lavee , Salomon Sickert

Chat View PDF

A Hierarchy of Nondeterminism

2022-01-01

Bader Abu Radi , Orna Kupferman , Ofer Leshkowitz

We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton $\mathcal{A}$ is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to $\mathcal{A}$ by removing … We study three levels in a hierarchy of nondeterminism: A nondeterministic automaton $\mathcal{A}$ is determinizable by pruning (DBP) if we can obtain a deterministic automaton equivalent to $\mathcal{A}$ by removing some of its transitions. Then, $\mathcal{A}$ is history deterministic (HD) if its nondeterministic choices can be resolved in a way that only depends on the past. Finally, $\mathcal{A}$ is semantically deterministic (SD) if different nondeterministic choices in $\mathcal{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 HD 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\"uchi, co-B\"uchi, 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. We relate the latter to nondeterministic automata that can be used when reasoning about probabilistic systems.

Chat View PDF

Certifying Inexpressibility

2021-03-22

Salomon Sickert , Orna Kupferman

Different classes of automata on infinite words have different expressive power.Deciding whether a given language L ⊆ Σ ω can be expressed by an automaton of a desired class can … Different classes of automata on infinite words have different expressive power.Deciding whether a given language L ⊆ Σ ω can be expressed by an automaton of a desired class can be reduced to deciding a game between Prover and Refuter: in each turn of the game, Refuter provides a letter in Σ, and Prover responds with an annotation of the current state of the run (for example, in the case of Büchi automata, whether the state is accepting or rejecting, and in the case of parity automata, what the color of the state is).Prover wins if the sequence of annotations she generates is correct: it is an accepting run iff the word generated by Refuter is in L. We show how a winning strategy for Refuter can serve as a simple and easy-to-understand certificate to inexpressibility, and how it induces additional forms of certificates.Our framework handles all classes of deterministic automata, including ones with structural restrictions like weak automata.In addition, it can be used for refuting separation of two languages by an automaton of the desired class, and for finding automata that approximate L and belong to the desired class.

Chat View PDF

Good-Enough Synthesis

2021-01-01

Shaull Almagor , Orna Kupferman

In the classical synthesis problem, we are given an LTL formula ψover sets of input and output signals, and we synthesize a system T that realizes ψ: with every input … In the classical synthesis problem, we are given an LTL formula ψover sets of input and output signals, and we synthesize a system T that realizes ψ: with every input sequences x, the system associates an output sequence T(x) such that the generated computation x \otimes T(x) satisfies ψ. In practice, the requirement to satisfy the specification in all environments is often too strong, and it is common to add assumptions on the environment. We introduce a new type of relaxation on this requirement. In good-enough synthesis (GE-synthesis), the system is required to generate a satisfying computation only if one exists. Formally, an input sequence x is hopeful if there exists some output sequence y such that the computation x \otimes y satisfies ψ, and a system GE-realizes ψif it generates a computation that satisfies ψon all hopeful input sequences. GE-synthesis is particularly relevant when the notion of correctness is multi-valued (rather than Boolean), and thus we seek systems of the highest possible quality, and when synthesizing autonomous systems, which interact with unexpected environments and are often only expected to do their best. We study GE-synthesis in Boolean and multi-valued settings. In both, we suggest and solve various definitions of GE-synthesis, corresponding to different ways a designer may want to take hopefulness into account. We show that in all variants, GE-synthesis is not computationally harder than traditional synthesis, and can be implemented on top of existing tools. Our algorithms are based on careful combinations of nondeterministic and universal automata. We augment systems that GE-realize their specifications by monitors that provide satisfaction information. In the multi-valued setting, we provide both a worst-case analysis and an expectation-based one, the latter corresponding to an interaction with a stochastic environment.

Chat View PDF

Certifying DFA Bounds for Recognition and Separation

2021-01-01

Orna Kupferman , Nir Lavee , Salomon Sickert

Chat View PDF

Certifying Inexpressibility

2021-01-01

Orna Kupferman , Salomon Sickert

Chat View PDF

Minimization and Canonization of GFG Transition-Based Automata

2021-01-01

Bader Abu Radi , Orna Kupferman

While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) automata. The latter are nondeterministic automata that can … While many applications of automata in formal methods can use nondeterministic automata, some applications, most notably synthesis, need deterministic or good-for-games (GFG) 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 deterministic Büchi and co-Büchi word automata is NP-complete. In particular, no canonical minimal deterministic automaton exists, and a language may have different minimal deterministic automata. We describe a polynomial minimization algorithm for GFG 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. We use our minimization algorithm to show canonicity for transition-based GFG co-Büchi word automata: all minimal automata have isomorphic safe components (namely components obtained by restricting the transitions to these not in $α$) and once we saturate the automata with $α$-transitions, we get full isomorphism.

Chat View PDF

Canonicity in GFG and Transition-Based Automata

2020-09-20

Bader Abu Radi , Orna Kupferman

Minimization of deterministic automata on finite words results in a {\em canonical\/} automaton. For deterministic automata on infinite words, no canonical minimal automaton exists, and a language may have different … Minimization of deterministic automata on finite words results in a {\em canonical\/} automaton. For deterministic automata on infinite words, no canonical minimal automaton exists, and a language may have different minimal deterministic B\"uchi (DBW) or co-B\"uchi (DCW) automata. In recent years, researchers have studied {\em good-for-games\/} (GFG) automata -- nondeterministic automata that can resolve their nondeterministic choices in a way that only depends on the past. Several applications of automata in formal methods, most notably synthesis, that are traditionally based on deterministic automata, can instead be based on GFG automata. The {\em minimization\/} problem for DBW and DCW is NP-complete, and it stays NP-complete for GFG B\"uchi and co-B\"uchi automata. On the other hand, minimization of GFG co-B\"uchi automata with {\em transition-based\/} acceptance (GFG-tNCWs) can be solved in polynomial time. In these automata, acceptance is defined by a set $\alpha$ of transitions, and a run is accepting if it traverses transitions in $\alpha$ only finitely often. This raises the question of canonicity of minimal deterministic and GFG automata with transition-based acceptance. In this paper we study this problem. We start with GFG-tNCWs and show that the safe components (that is, these obtained by restricting the transitions to these not in $\alpha$) of all minimal GFG-tNCWs are isomorphic, and that by saturating the automaton with transitions in $\alpha$ we get isomorphism among all minimal GFG-tNCWs. Thus, a canonical form for minimal GFG-tNCWs can be obtained in polynomial time. We continue to DCWs with transition-based acceptance (tDCWs), and their dual tDBWs. We show that here, while no canonical form for minimal automata exists, restricting attention to the safe components is useful, and implies that the only minimal tDCWs that have no canonical form are these for which the transition to the GFG model results in strictly smaller automaton, which do have a canonical minimal form.

Chat View PDF

Reasoning about Quality and Fuzziness of Strategic Behaviours

2019-07-28

Patricia Bouyer , Orna Kupferman , Nicolas Markey +3 more

We introduce and study SL[F], a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula … We introduce and study SL[F], a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an SL[F] formula is a real value in [0,1], reflecting ``how much'' or ``how well'' the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of SL[F] in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for ourlogic, based on a quantitative extension of Quantified CTL*.

Chat View PDF

Reasoning about Quality and Fuzziness of Strategic Behaviours

2019-01-01

Patricia Bouyer , Orna Kupferman , Nicolas Markey +3 more

Temporal logics are extensively used for the specification of on-going behaviours of reactive systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that … Temporal logics are extensively used for the specification of on-going behaviours of reactive systems. Two significant developments in this area are the extension of traditional temporal logics with modalities that enable the specification of on-going strategic behaviours in multi-agent systems, and the transition of temporal logics to a quantitative setting, where different satisfaction values enable the specifier to formalise concepts such as certainty or quality. We introduce and study FSL---a quantitative extension of SL (Strategy Logic), one of the most natural and expressive logics describing strategic behaviours. The satisfaction value of an FSL formula is a real value in [0,1], reflecting `how much' or `how well' the strategic on-going objectives of the underlying agents are satisfied. We demonstrate the applications of FSL in quantitative reasoning about multi-agent systems, by showing how it can express concepts of stability in multi-agent systems, and how it generalises some fuzzy temporal logics. We also provide a model-checking algorithm for our logic, based on a quantitative extension of Quantified CTL*.

Chat View PDF

Timed Network Games with Clocks

2018-08-14

Guy Avni , Shibashis Guha , Orna Kupferman

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 … 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 {\em 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 \cite{AGK17}, we introduced {\em 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 {\em 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 \cite{AGK17} and we develop new techniques in order to show that positive results on classic network games carry over to the stronger timed setting.

Chat View PDF

Timed network games with clocks

2018-08-01

Guy Avni , Shibashis Guha , Orna Kupferman

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 … 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.

Flow Logic

2018-06-15

Orna Kupferman , Gal Vardi

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. Many of these applications … 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. 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 \mathbb{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. 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 ${\rm P}^{\rm 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. Finally, we introduce and study the query-checking problem for BFL*, where under-specified BFL* formulas are used for network exploration.

Chat View PDF

Timed Network Games with Clocks

2018-01-01

Guy Avni , Shibashis Guha , Orna Kupferman

Chat View PDF

Flow Logic

2018-01-01

Orna Kupferman , Gal Vardi

Chat View PDF

How Deterministic are Good-For-Games Automata?

2017-10-11

Udi Boker , Orna Kupferman , Michał Skrzypczak

In 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 … In 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 Buchi and co-Buchi 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 Buchi or co-Buchi 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.

How Deterministic are Good-For-Games Automata?

2017-01-01

Udi Boker , Orna Kupferman , Michał Skrzypczak

Chat View PDF

High-Quality Synthesis Against Stochastic Environments

2016-08-23

Shaull Almagor , Orna Kupferman

In the classical synthesis problem, we are given an LTL formula psi over sets of input and output signals, and we synthesize a transducer that realizes psi. One weakness of … In the classical synthesis problem, we are given an LTL formula psi over sets of input and output signals, and we synthesize a transducer that realizes 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 LTL[F] is a multi-valued logic that augments LTL with quality operators. The satisfaction value of an LTL[F] 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 LFL[F]. 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, and remains so 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.

Chat View PDF

Minimizing Expected Cost Under Hard Boolean Constraints, with Applications to Quantitative Synthesis

2016-01-01

Shaull Almagor , Orna Kupferman , Yaron Velner

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 … 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 $ω$-regular condition against an adversarial environment. We consider the case the $ω$-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 $ε$-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 $ω$-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.

Chat View PDF

High-Quality Synthesis Against Stochastic Environments

2016-01-01

Shaull Almagor , Orna Kupferman

Chat View PDF

Profile trees for Büchi word automata, with application to determinization

2015-06-25

Seth Fogarty , Orna Kupferman , Moshe Y. Vardi +1 more

Chat View PDF

Discounting in LTL

2014-06-17

Shaull Almagor , Udi Boker , Orna Kupferman

In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the … In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of \emph{how well} the system satisfies the specification. One direction in this effort is to refine the eventually operators of temporal logic to {\em discounting operators}: the satisfaction value of a specification is a value in $[0,1]$, where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is. In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.

Chat View PDF

Discounting in LTL

2014-01-01

Shaull Almagor , Udi Boker , Orna Kupferman

In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the … In recent years, there is growing need and interest in formalizing and reasoning about the quality of software and hardware systems. As opposed to traditional verification, where one handles the question of whether a system satisfies, or not, a given specification, reasoning about quality addresses the question of \emph{how well} the system satisfies the specification. One direction in this effort is to refine the "eventually" operators of temporal logic to {\em discounting operators}: the satisfaction value of a specification is a value in $[0,1]$, where the longer it takes to fulfill eventuality requirements, the smaller the satisfaction value is. In this paper we introduce an augmentation by discounting of Linear Temporal Logic (LTL), and study it, as well as its combination with propositional quality operators. We show that one can augment LTL with an arbitrary set of discounting functions, while preserving the decidability of the model-checking problem. Further augmenting the logic with unary propositional quality operators preserves decidability, whereas adding an average-operator makes some problems undecidable. We also discuss the complexity of the problem, as well as various extensions.

Chat View PDF

Profile Trees for Büchi Word Automata, with Application to Determinization

2013-07-15

Seth Fogarty , Orna Kupferman , Moshe Y. Vardi +1 more

The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by … The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally.

Chat View PDF

Unifying B\"uchi Complementation Constructions

2013-03-27

Seth Fogarty , Orna Kupferman , Thomas Wilke +1 more

Complementation of B\"uchi 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 … Complementation of B\"uchi 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 K\"ahler 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 the tight bound of Schewe's construction

Chat View PDF

Rational Synthesis

2009-07-17

Dana Fisman , Orna Kupferman , Yoad Lustig

Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or … Synthesis is the automated construction of a system from its specification. The system has to satisfy its specification in all possible environments. Modern systems often interact with other systems, or agents. Many times these agents have objectives of their own, other than to fail the system. Thus, it makes sense to model system environments not as hostile, but as composed of rational agents; i.e., agents that act to achieve their own objectives. We introduce the problem of synthesis in the context of rational agents (rational synthesis, for short). The input consists of a temporal-logic formula specifying the system and temporal-logic formulas specifying the objectives of the agents. The output is an implementation T of the system and a profile of strategies, suggesting a behavior for each of the agents. The output should satisfy two conditions. First, the composition of T with the strategy profile should satisfy the specification. Second, the strategy profile should be an equilibria in the sense that, in view of their objectives, agents have no incentive to deviate from the strategies assigned to them. We solve the rational-synthesis problem for various definitions of equilibria studied in game theory. We also consider the multi-valued case in which the objectives of the system and the agents are still temporal logic formulas, but involve payoffs from a finite lattice.

Chat View PDF

Rational Synthesis

2009-01-01

Dana Fisman , Orna Kupferman , Yoad Lustig

Chat View PDF

What causes a system to satisfy a specification?

2008-06-01

Hana Chockler , Joseph Y. Halpern , Orna Kupferman

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers … Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this article, we relate a formal definition of causality given by Halpern and Pearl to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion of responsibility , which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.

Chat View PDF

What Causes a System to Satisfy a Specification?

2003-01-01

Hana Chockler , Joseph Y. Halpern , Orna Kupferman

Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers … Even when a system is proven to be correct with respect to a specification, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. Coverage metrics attempt to check which parts of a system are actually relevant for the verification process to succeed. Recent work on coverage in model checking suggests several coverage metrics and algorithms for finding parts of the system that are not covered by the specification. The work has already proven to be effective in practice, detecting design errors that escape early verification efforts in industrial settings. In this paper, we relate a formal definition of causality given by Halpern and Pearl [2001] to coverage. We show that it gives significant insight into unresolved issues regarding the definition of coverage and leads to potentially useful extensions of coverage. In particular, we introduce the notion of responsibility, which assigns to components of a system a quantitative measure of their relevance to the satisfaction of the specification.

Chat View PDF

Common Coauthors

Coauthor	Papers Together
Shaull Almagor	6
Bader Abu Radi	5
Udi Boker	4
Salomon Sickert	4
Shibashis Guha	3
Moshe Y. Vardi	3
Seth Fogarty	3
Guy Avni	3
Thomas Wilke	3
Ofer Leshkowitz	3
Patricia Bouyer	2
Dana Fisman	2
Bastien Maubert	2
Gal Vardi	2
Yoad Lustig	2
Giuseppe Perelli	2
Michał Skrzypczak	2
Nicolas Markey	2
Joseph Y. Halpern	2
Nir Lavee	2
Hana Chockler	2
Aniello Murano	2
Noam Shenwald	1
Orna Grümberg	1
Yoav Feinstein	1
Sarai Sheinvald	1
Yaron Velner	1
Namma Shamash Halevy	1

Commonly Cited References

Efficient Separability of Regular Languages by Subsequences and Suffixes

2013-01-01

Wojciech Czerwiński , Wim Martens , Tomáš Masopust

Chat View PDF

Büchi Complementation Made Tight

2009-02-26

Sven Schewe

The precise complexity of complementing B\uchi automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple -- it suffices to determinize them using … The precise complexity of complementing B\uchi automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple -- it suffices to determinize them using a simple subset construction and to dualize the acceptance condition of the resulting automaton -- B\uchi complementation is more involved. Indeed, the construction of an EXPTIME complementation procedure took a quarter of a century from the introduction of B\uchi automata in the early $60$s, and stepwise narrowing the gap between the upper and lower bound to a simple exponent (of $(6e)^n$ for B\uchi automata with $n$ states) took four decades. While the distance between the known upper ($O\big((0.96\,n)^n\big)$) and lower ($\Omega\big((0.76\,n)^n\big)$) bound on the required number of states has meanwhile been significantly reduced, an exponential factor remains between them. Also, the upper bound on the size of the complement automaton is not linear in the bound of its state space. These gaps are unsatisfactory from a theoretical point of view, but also because B\uchi complementation is a useful tool in formal verification, in particular for the language containment problem. This paper proposes a B\uchi complementation algorithm whose complexity meets, modulo a quadratic ($O(n^2)$) factor, the known lower bound for B\uchi complementation. It thus improves over previous constructions by an exponential factor and concludes the quest for optimal B\uchi complementation algorithms.

Chat View PDF

Certifying Inexpressibility

2021-03-22

Salomon Sickert , Orna Kupferman

Chat View PDF

Büchi complementation made tight

2009-01-01

Sven Schewe

The precise complexity of complementing Büchi automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple - it suffices to determinize them using … The precise complexity of complementing Büchi automata is an intriguing and long standing problem. While optimal complementation techniques for finite automata are simple - it suffices to determinize them using a simple subset construction and to dualize the acceptance condition of the resulting automaton - Büchi complementation is more involved. Indeed, the construction of an EXPTIME complementation procedure took a quarter of a century from the introduction of Büchi automata in the early 60s, and stepwise narrowing the gap between the upper and lower bound to a simple exponent (of (6e)n for Büchi automata with n states) took four decades. While the distance between the known upper (O'(0.96 n)n') and lower ('(0.76 n)n') bound on the required number of states has meanwhile been significantly reduced, an exponential factor remains between them. Also, the upper bound on the size of the complement automaton is not linear in the bound of its state space. These gaps are unsatisfactory from a theoretical point of view, but also because Büchi complementation is a useful tool in formal verification, in particular for the language containment problem. This paper proposes a Büchi complementation algorithm whose complexity meets, modulo a quadratic (O(n2)) factor, the known lower bound for Büchi complementation. It thus improves over previous constructions by an exponential factor and concludes the quest for optimal Büchi complementation algorithms.

Chat View PDF

Explainable Reactive Synthesis

2020-01-01

Tom Baumeister , Bernd Finkbeiner , Hazem Torfah

Chat View PDF

Certifying Inexpressibility

2021-01-01

Orna Kupferman , Salomon Sickert

Chat View PDF

From Nondeterministic Buchi and Streett Automata to Deterministic Parity Automata

2006-09-22

Nir Piterman

In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi … In this paper we revisit Safra's determinization constructions. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Specifically, starting from a nondeterministic Buchi automaton with n states our construction yields a deterministic parity automaton with n 2n+2 states and index 2n (instead of a Rabin automaton with (12) n n 2n states and n pairs). Starting from a nondeterministic Streett automaton with n states and k pairs our construction yields a deterministic parity automaton with n n(k+2)+2 (k+1) 2n(K+1) states and index 2n(k+1) (instead of a Rabin automaton with (12) n(k+1) n n(k+2) (k+1) 2n(k+1) states and n(k+1) pairs). The parity condition is much simpler than the Rabin condition. In applications such as solving games and emptiness of tree automata handling the Rabin condition involves an additional multiplier of n 2 n!(or(n(k+1)) 2 (n(k+1))! in the case of Streett) which is saved using our construction

Chat View PDF

Minimising Good-for-Games automata is NP complete

2020-01-01

Sven Schewe

This paper discusses the hardness of finding minimal good-for-games (GFG) Buchi, Co-Buchi, and parity automata with state based acceptance. The problem appears to sit between finding small deterministic and finding … This paper discusses the hardness of finding minimal good-for-games (GFG) Buchi, Co-Buchi, and parity automata with state based acceptance. The problem appears to sit between finding small deterministic and finding small nondeterministic automata, where minimality is NP-complete and PSPACE-complete, respectively. However, recent work of Radi and Kupferman has shown that minimising Co-Buchi automata with transition based acceptance is tractable, which suggests that the complexity of minimising GFG automata might be cheaper than minimising deterministic automata. We show for the standard state based acceptance that the minimality of a GFG automaton is NP-complete for Buchi, Co-Buchi, and parity GFG automata. The proofs are a surprisingly straight forward generalisation of the proofs from deterministic Buchi automata: they use a similar reductions, and the same hard class of languages.

Chat View PDF

State of Büchi Complementation

2011-01-01

Ming-Hsien Tsai , Seth Fogarty , Moshe Y. Vardi +1 more

Chat View PDF

Environment Assumptions for Synthesis

2008-01-01

Krishnendu Chatterjee , Thomas A. Henzinger , Barbara Jobstmann

Regular Separability of Well Structured Transition Systems

2017-01-01

Wojciech Czerwiński , Sławomir Lasota , Roland Meyer +3 more

We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are … We investigate the languages recognized by well-structured transition systems (WSTS) with upward and downward compatibility. Our first result shows that, under very mild assumptions, every two disjoint WSTS languages are regular separable: There is a regular language containing one of them and being disjoint from the other. As a consequence, if a language as well as its complement are both recognized by WSTS, then they are necessarily regular. In particular, no subclass of WSTS languages beyond the regular languages is closed under complement. Our second result shows that for Petri nets, the complexity of the backwards coverability algorithm yields a bound on the size of the regular separator. We complement it by a lower bound construction.

Chat View PDF

Strategy logic with imperfect information

2017-06-01

Raphaël Berthon , Bastien Maubert , Aniello Murano +2 more

We introduce an extension of Strategy logic for the imperfect-information setting, called SL ii , and study its model-checking problem. As this logic naturally captures multi-player games with … We introduce an extension of Strategy logic for the imperfect-information setting, called SL ii , and study its model-checking problem. As this logic naturally captures multi-player games with imperfect information, the problem turns out to be undecidable. We introduce a syntactical class of "hierarchical instances" for which, intuitively, as one goes down the syntactic tree of the formula, strategy quantifications are concerned with finer observations of the model. We prove that model-checking SL ii restricted to hierarchical instances is decidable. This result, because it allows for complex patterns of existential and universal quantification on strategies, greatly generalises previous ones, such as decidability of multi-player games with imperfect information and hierarchical observations, and decidability of distributed synthesis for hierarchical systems. To establish the decidability result, we introduce and study QCTL ii *, an extension of QCTL (itself an extension of CTL with second-order quantification over atomic propositions) by parameterising its quantifiers with observations. The simple syntax of QCTL ii * allows us to provide a conceptually neat reduction of SL ii to QCTL ii * that separates concerns, allowing one to forget about strategies and players and focus solely on second-order quantification. While the model-checking problem of QCTL ii * is, in general, undecidable, we identify a syntactic fragment of hierarchical formulas and prove, using an automata-theoretic approach, that it is decidable. The decidability result for SL ii follows since the reduction maps hierarchical instances of SL ii to hierarchical formulas of QCTL ii *.

Chat View PDF

Approximate Automata for Omega-Regular Languages

2019-01-01

Rayna Dimitrova , Bernd Finkbeiner , Hazem Torfah

Chat View PDF

Separating Regular Languages with First-Order Logic

2016-03-09

Thomas Place , Marc Zeitoun

Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular … Given two languages, a separator is a third language that contains the first one and is disjoint from the second one. We investigate the following decision problem: given two regular input languages of finite words, decide whether there exists a first-order definable separator. We prove that in order to answer this question, sufficient information can be extracted from semigroups recognizing the input languages, using a fixpoint computation. This yields an EXPTIME algorithm for checking first-order separability. Moreover, the correctness proof of this algorithm yields a stronger result, namely a description of a possible separator. Finally, we generalize this technique to answer the same question for regular languages of infinite words.

Chat View PDF

Causes and Explanations: A Structural-Model Approach. Part I: Causes

2005-11-09

Joseph Y. Halpern , Judea Pearl

We propose a new definition of actual causes, using structural equations to model counterfactuals. We show that the definition yields a plausible and elegant account of causation that handles well … We propose a new definition of actual causes, using structural equations to model counterfactuals. We show that the definition yields a plausible and elegant account of causation that handles well examples which have caused problems for other definitions and resolves major difficulties in the traditional account. 1. Introduction 2. Causal models: a review2.1Causal models 2.2Syntax and semantics 3. The definition of cause 4. Examples 5. A more refined definition 6. Discussion AAppendix: Some Technical Issues A.1The active causal process A.2A closer look at AC2(b) A.3Causality with infinitely many variables A.4Causality in nonrecursive models

Chat View PDF

A strongly polynomial minimum cost circulation algorithm

1985-09-01

Éva Tardos

Cooperative Reactive Synthesis

2015-01-01

Roderick Bloem , Rüdiger Ehlers , Robert Könighofer

Chat View PDF

Some Complexity Results for Stateful Network Verification

2016-01-01

Yaron Velner , Kalev Alpernas , Aurojit Panda +4 more

Chat View PDF

Introduction to Algorithms

1991-09-01

V. J. Rayward‐Smith , Thomas H. Cormen , Charles E. Leiserson +1 more

Unifying B\"uchi Complementation Constructions

2013-03-27

Seth Fogarty , Orna Kupferman , Thomas Wilke +1 more

Chat View PDF

Reasoning about Quality and Fuzziness of Strategic Behaviours

2019-07-28

Patricia Bouyer , Orna Kupferman , Nicolas Markey +3 more

Chat View PDF

Energy and Mean-Payoff Parity Markov Decision Processes

2011-04-14

Krishnendu Chatterjee , Laurent Doyen

We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode \omega-regular specifications, and the mean-payoff and energy … We consider Markov Decision Processes (MDPs) with mean-payoff parity and energy parity objectives. In system design, the parity objective is used to encode \omega-regular specifications, and the mean-payoff and energy objectives can be used to model quantitative resource constraints. The energy condition requires that the resource level never drops below 0, and the mean-payoff condition requires that the limit-average value of the resource consumption is within a threshold. While these two (energy and mean-payoff) classical conditions are equivalent for two-player games, we show that they differ for MDPs. We show that the problem of deciding whether a state is almost-sure winning (i.e., winning with probability 1) in energy parity MDPs is in NP \cap coNP, while for mean-payoff parity MDPs, the problem is solvable in polynomial time, improving a recent PSPACE bound.

Chat View PDF

On Subgame Perfection in Quantitative Reachability Games

2012-05-29

Thomas Brihaye , Véronique Bruyère , Julie De Pril +1 more

We study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In such games, each player aims at reaching his own goal set of states as … We study turn-based quantitative multiplayer non zero-sum games played on finite graphs with reachability objectives. In such games, each player aims at reaching his own goal set of states as soon as possible. A previous work on this model showed that Nash equilibria (resp. secure equilibria) are guaranteed to exist in the multiplayer (resp. two-player) case. The existence of secure equilibria in the multiplayer case remained and is still an open problem. In this paper, we focus our study on the concept of subgame perfect equilibrium, a refinement of Nash equilibrium well-suited in the framework of games played on graphs. We also introduce the new concept of subgame perfect secure equilibrium. We prove the existence of subgame perfect equilibria (resp. subgame perfect secure equilibria) in multiplayer (resp. two-player) quantitative reachability games. Moreover, we provide an algorithm deciding the existence of secure equilibria in the multiplayer case.

Chat View PDF

Responsibility and blame: a structural-model approach

2003-01-01

Hana Chockler , Joseph Y. Halpern

Causality is typically treated an all-or-nothing concept; either A is a cause of B or it is not. We extend the definition of causality introduced by Halpern and Pearl [2001] … Causality is typically treated an all-or-nothing concept; either A is a cause of B or it is not. We extend the definition of causality introduced by Halpern and Pearl [2001] to take into account the degree of responsibility of A for B. For example, if someone wins an election 11--0, then each person who votes for him is less responsible for the victory than if he had won 6--5. We then define a notion of degree of blame, which takes into account an agent's epistemic state. Roughly speaking, the degree of blame of A for B is the expected degree of responsibility of A for B, taken over the epistemic state of an agent.

Chat View PDF

Multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives

2015-04-30

Lorenzo Clemente , Jean-François Raskin

The beyond worst-case threshold problem (BWC), recently introduced by Bruy\`ere et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level … The beyond worst-case threshold problem (BWC), recently introduced by Bruy\`ere et al., asks given a quantitative game graph for the synthesis of a strategy that i) enforces some minimal level of performance against any adversary, and ii) achieves a good expectation against a stochastic model of the adversary. They solved the BWC problem for finite-memory strategies and unidimensional mean-payoff objectives and they showed membership of the problem in NP$\cap$coNP. They also noted that infinite-memory strategies are more powerful than finite-memory ones, but the respective threshold problem was left open. We extend these results in several directions. First, we consider multidimensional mean-payoff objectives. Second, we study both finite-memory and infinite-memory strategies. We show that the multidimensional BWC problem is coNP-complete in both cases. Third, in the special case when the worst-case objective is unidimensional (but the expectation objective is still multidimensional) we show that the complexity decreases to NP$\cap$coNP. This solves the infinite-memory threshold problem left open by Bruy\`ere et al., and this complexity cannot be improved without improving the currently known complexity of classical mean-payoff games. Finally, we introduce a natural relaxation of the BWC problem, the beyond almost-sure threshold problem (BAS), which asks for the synthesis of a strategy that ensures some minimal level of performance with probability one and a good expectation against the stochastic model of the adversary. We show that the multidimensional BAS threshold problem is solvable in P.

Chat View PDF

Timed Parity Games: Complexity and Robustness

2011-12-14

Krishnendu Chatterjee , Thomas A. Henzinger , Vinayak S. Prabhu

We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are \emph{concurrent} in that at … We consider two-player games played in real time on game structures with clocks where the objectives of players are described using parity conditions. The games are \emph{concurrent} in that at each turn, both players independently propose a time delay and an action, and the action with the shorter delay is chosen. To prevent a player from winning by blocking time, we restrict each player to play strategies that ensure that the player cannot be responsible for causing a zeno run. First, we present an efficient reduction of these games to \emph{turn-based} (i.e., not concurrent) \emph{finite-state} (i.e., untimed) parity games. Our reduction improves the best known complexity for solving timed parity games. Moreover, the rich class of algorithms for classical parity games can now be applied to timed parity games. The states of the resulting game are based on clock regions of the original game, and the state space of the finite game is linear in the size of the region graph. Second, we consider two restricted classes of strategies for the player that represents the controller in a real-time synthesis problem, namely, \emph{limit-robust} and \emph{bounded-robust} winning strategies. Using a limit-robust winning strategy, the controller cannot choose an exact real-valued time delay but must allow for some nonzero jitter in each of its actions. If there is a given lower bound on the jitter, then the strategy is bounded-robust winning. We show that exact strategies are more powerful than limit-robust strategies, which are more powerful than bounded-robust winning strategies for any bound. For both kinds of robust strategies, we present efficient reductions to standard timed automaton games. These reductions provide algorithms for the synthesis of robust real-time controllers.

Chat View PDF

Environment Assumptions for Synthesis

2008-01-01

Krishnendu Chatterjee , Thomas A. Henzinger , Barbara Jobstmann

The synthesis problem asks to construct a reactive finite-state system from an $ω$-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. … The synthesis problem asks to construct a reactive finite-state system from an $ω$-regular specification. Initial specifications are often unrealizable, which means that there is no system that implements the specification. A common reason for unrealizability is that assumptions on the environment of the system are incomplete. We study the problem of correcting an unrealizable specification $ϕ$ by computing an environment assumption $ψ$ such that the new specification $ψ\toϕ$ is realizable. Our aim is to construct an assumption $ψ$ that constrains only the environment and is as weak as possible. We present a two-step algorithm for computing assumptions. The algorithm operates on the game graph that is used to answer the realizability question. First, we compute a safety assumption that removes a minimal set of environment edges from the graph. Second, we compute a liveness assumption that puts fairness conditions on some of the remaining environment edges. We show that the problem of finding a minimal set of fair edges is computationally hard, and we use probabilistic games to compute a locally minimal fairness assumption.

Chat View PDF

Better Quality in Synthesis through Quantitative Objectives

2009-04-17

Roderick Bloem , Krishnendu Chatterjee , Thomas A. Henzinger +1 more

Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every … Most specification languages express only qualitative constraints. However, among two implementations that satisfy a given specification, one may be preferred to another. For example, if a specification asks that every request is followed by a response, one may prefer an implementation that generates responses quickly but does not generate unnecessary responses. We use quantitative properties to measure the goodness of an implementation. Using games with corresponding quantitative objectives, we can synthesize implementations, which are preferred among the set of possible implementations that satisfy a given specification. In particular, we show how automata with lexicographic mean-payoff conditions can be used to express many interesting quantitative properties for reactive systems. In this framework, the synthesis of optimal implementations requires the solution of lexicographic mean-payoff games (for safety requirements), and the solution of games with both lexicographic mean-payoff and parity objectives (for liveness requirements). We present algorithms for solving both kinds of novel graph games.

Chat View PDF

Reasoning About Strategies: On the Model-Checking Problem

2011-01-01

Fabio Mogavero , Aniello Murano , Giuseppe Perelli +1 more

In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how … In open systems verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. An important contribution in this context is given by modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL\star, and the like. Recently, Chatterjee, Henzinger, and Piterman introduced Strategy Logic, which we denote here by CHP-SL, with the aim of getting a powerful framework for reasoning explicitly about strategies. CHP-SL is obtained by using first-order quantifications over strategies and has been investigated in the very specific setting of two-agents turned-based games, where a non-elementary model-checking algorithm has been provided. While CHP-SL is a very expressive logic, we claim that it does not fully capture the strategic aspects of multi-agent systems. In this paper, we introduce and study a more general strategy logic, denoted SL, for reasoning about strategies in multi-agent concurrent games. We prove that SL includes CHP-SL, while maintaining a decidable model-checking problem. In particular, the algorithm we propose is computationally not harder than the best one known for CHP-SL. Moreover, we prove that such a problem for SL is NonElementarySpace-hard. This negative result has spurred us to investigate here syntactic fragments of SL, strictly subsuming ATL\star, with the hope of obtaining an elementary model-checking problem. Among the others, we study the sublogics SL[NG], SL[BG], and SL[1G]. They encompass formulas in a special prenex normal form having, respectively, nested temporal goals, Boolean combinations of goals and, a single goal at a time. About these logics, we prove that the model-checking problem for SL[1G] is 2ExpTime-complete, thus not harder than the one for ATL\star.

Chat View PDF

From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata

2007-08-14

Nir Piterman

In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization … In this paper we revisit Safra's determinization constructions for automata on infinite words. We show how to construct deterministic automata with fewer states and, most importantly, parity acceptance conditions. Determinization is used in numerous applications, such as reasoning about tree automata, satisfiability of CTL*, and realizability and synthesis of logical specifications. The upper bounds for all these applications are reduced by using the smaller deterministic automata produced by our construction. In addition, the parity acceptance conditions allows to use more efficient algorithms (when compared to handling Rabin or Streett acceptance conditions).

Chat View PDF

Causes and Explanations: A Structural-Model Approach

2000-11-07

Joseph Y. Halpern , Judea Pearl

In Proceedings of the Seventeenth Conference on Uncertainy in Artiﬁcial Intelligence, San Francisco, CA: Morgan Kaufmann, 194–202, 2001. TECHNICAL REPORT R-266-UAI June 2001 Causes and Explanations: A Structural-Model Approach— Part … In Proceedings of the Seventeenth Conference on Uncertainy in Artiﬁcial Intelligence, San Francisco, CA: Morgan Kaufmann, 194–202, 2001. TECHNICAL REPORT R-266-UAI June 2001 Causes and Explanations: A Structural-Model Approach— Part I: Causes Joseph Y. Halpern Judea Pearl Cornell University Dept. of Computer Science Dept. of Computer Science University of California, Los Angeles Ithaca, NY 14853 Los Angeles, CA 90095 [email protected] [email protected] http://www.cs.cornell.edu/home/halpern http://www.cs.ucla.edu/ judea Abstract We propose a new deﬁnition of actual causes, using structural equations to model counterfac- tuals. We show that the deﬁnition yields a plausi- ble and elegant account of causation that handles well examples which have caused problems for other deﬁnitions and resolves major difﬁculties in the traditional account. 1 Introduction What does it mean that an event actually causes event ? This is a question that goes beyond mere philosophical speculation. As Good [1993] argues persuasively, in many legal settings, what needs to be established (for determin- ing responsibility) is not a counterfactual kind of causation, but “cause in fact.” A typical example considers two ﬁres advancing toward a house. If ﬁre burned the house be- fore ﬁre , we (and many juries nationwide) would con- sider ﬁre “the actual cause” for the damage, even sup- posing the house would have deﬁnitely burned down by ﬁre , if it were not for . Actual causation is also im- portant in artiﬁcial intelligence applications. Whenever we undertake to explain a set of events that unfold in a speciﬁc scenario, the explanation produced must acknowledge the actual cause of those events. The automatic generation of adequate explanations, a task essential in planning, diag- nosis and natural language processing, therefore requires a formal analysis of the concept of actual cause. Giving a precise and useful deﬁnition of actual causality is notoriously difﬁcult. The philosophical literature has been struggling with this notion since the days of Hume [1739]. (See [Sosa and Tooley 1993], [Hall 1998], and [Pearl 2000] for some recent discussions.) To borrow just one example from Hall [1998], suppose a bolt lightning hits a tree and Supported in part by NSF under grant IRI-96-25901 Supported in part by grants from NSF, ONR, AFOSR, and MICRO. starts a forest ﬁre. It seems reasonable to say that the light- ning bolt is a cause of the ﬁre. (Indeed, the description “the lightning bolt . . . starts a forest ﬁre” can be viewed as say- ing this.) But what about the oxygen in the air and the fact that the wood was dry? Presumably, if there has not been oxygen or the wood was wet there would not have been a ﬁre. Carrying this perhaps to the point of absurdity, what about the Big Bang? This problem is relatively easy to deal with, but there are a host of other, far more subtle, difﬁcul- ties that have been raised over the years. Here we give a deﬁnition of actual causality based on the language of structural equations; in a companion paper ([Halpern and Pearl 2001]; see also the full paper [Halpern and Pearl 2000]), we give a deﬁnition of (causal) explana- tion using the deﬁnition of causality. The use of structural equations as a model for causal relationships is standard in the social sciences, and seems to go back to the work of Se- wall Wright in the 1920s (see [Goldberger 1972] for a dis- cussion); the framework we use here is due to Pearl [1995], and is further developed in [Galles and Pearl 1997; Halpern 2000; Pearl 2000]. While it is hard to argue that our deﬁ- nition (or any other deﬁnition, for that matter) is the “right deﬁnition”, we show that it deals well with the difﬁculties that have plagued other approaches in the past, especially those exempliﬁed by the rather extensive compendium of Hall [1998]. There has been extensive discussion about causality in the literature, particularly in the philosophy literature. To keep this paper to manageable length, we spend only minimal time describing other approaches and comparing ours to them. We refer the reader to [Hall 1998; Pearl 2000; Sosa and Tooley 1993; Spirtes, Glymour, and Scheines 1993] for details and criticism of the probabilistic and logical ap- proaches to causality in the philosophy literature. (We do try to point out where our deﬁnition does better than per- haps the best known approach, due to Lewis [1986, 2000] in the course of discussing the examples.) There has also been work in the AI literature on causality. Perhaps the closest to this are papers by Pearl and his col- leagues that use the structural-model approach. The def-

Chat View PDF

Computing Maximum Flow with Augmenting Electrical Flows

2016-10-01

Aleksander Mądry

We present an Õ (m 7/10 U 1/7)-time algorithm for the maximum s-t flow problem (and the minimum s-t cut problem) in directed graphs with m arcs and largest integer … We present an Õ (m 7/10 U 1/7)-time algorithm for the maximum s-t flow problem (and the minimum s-t cut problem) in directed graphs with m arcs and largest integer capacity U. This matches the running time of the Õ (mU)10/7)- time algorithm of Madry [30] in the unit-capacity case, and improves over it, as well as over the Õ (m√n log U)-time algorithm of Lee and Sidford [25], whenever U is moderately large and the graph is sufficiently sparse. By well-known reductions, this also implies similar running time improvements for the maximum-cardinality bipartite b-matching problem. One of the advantages of our algorithm is that it is significantly simpler than the ones presented in [30] and [25]. In particular, these algorithms employ a sophisticated interior-point method framework, while our algorithm is cast directly in the classic augmenting path setting that almost all the combinatorial maximum flow algorithms use. At a high level, the presented algorithm takes a primal dual approach in which each iteration uses electrical flows computations both to find an augmenting s-t flow in the current residual graph and to update the dual solution. We show that by maintain certain careful coupling of these primal and dual solutions we are always guaranteed to make significant progress.

Chat View PDF

Good for Games Automata: From Nondeterminism to Alternation

2019-01-01

Udi Boker , Karoliina Lehtinen

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

Chat View PDF

Minimising Good-for-Games automata is NP complete

2020-03-26

Sven Schewe

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

2020-01-01

Udi Boker , Denis Kuperberg , Karoliina Lehtinen +1 more

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

Chat View PDF

Mean-Payoff Games on Timed Automata

2016-01-01

Shibashis Guha , Marcin Jurdziński , Shankara Narayanan Krishna +1 more

Mean-payoff games on timed automata are played on the infinite weighted graph of configurations of priced timed automata between two players, Player Min and Player Max, by moving a token … Mean-payoff games on timed automata are played on the infinite weighted graph of configurations of priced timed automata between two players, Player Min and Player Max, by moving a token along the states of the graph to form an infinite run. The goal of Player Min is to minimize the limit average weight of the run, while the goal of the Player Max is the opposite. Brenguier, Cassez, and Raskin recently studied a variation of these games and showed that mean-payoff games are undecidable for timed automata with five or more clocks. We refine this result by proving the undecidability of mean-payoff games with three clocks. On a positive side, we show the decidability of mean-payoff games on one-clock timed automata with binary price-rates. A key contribution of this paper is the application of dynamic programming based proof techniques applied in the context of average reward optimization on an uncountable state and action space.

Chat View PDF

Learning nominal automata

2016-12-22

Joshua Moerman , Matteo Sammartino , Alexandra Silva +2 more

We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations … We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting. In particular we can learn a subclass of nominal non-deterministic automata. An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments.

Chat View PDF

Canonicity in GFG and Transition-Based Automata

2020-09-20

Bader Abu Radi , Orna Kupferman

Chat View PDF

Automata theory in nominal sets

2014-08-15

Mikołaj Bojańczyk , Bartek Klin , Sławomir Lasota

We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, … We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.

Chat View PDF

Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique

2008-03-19

Qiqi Yan

In this paper, we first introduce a lower bound technique for the state complexity of transformations of automata. Namely we suggest first considering the class of full automata in lower … In this paper, we first introduce a lower bound technique for the state complexity of transformations of automata. Namely we suggest first considering the class of full automata in lower bound analysis, and later reducing the size of the large alphabet via alphabet substitutions. Then we apply such technique to the complementation of nondeterministic \omega-automata, and obtain several lower bound results. Particularly, we prove an \omega((0.76n)^n) lower bound for B\"uchi complementation, which also holds for almost every complementation or determinization transformation of nondeterministic omega-automata, and prove an optimal (\omega(nk))^n lower bound for the complementation of generalized B\"uchi automata, which holds for Streett automata as well.

Chat View PDF

Certifying DFA Bounds for Recognition and Separation

2022-03-15

Orna Kupferman , Nir Lavee , Salomon Sickert

Chat View PDF

Multi-valued Verification of Strategic Ability

2020-11-11

Wojciech Jamroga , Beata Konikowska , Damian Kurpiewski +1 more

Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of … Some multi-agent scenarios call for the possibility of evaluating specifications in a richer domain of truth values. Examples include runtime monitoring of a temporal property over a growing prefix of an infinite path, inconsistency analysis in distributed databases, and verification methods that use incomplete anytime algorithms, such as bounded model checking. In this paper, we present multi-valued alternating-time temporal logic (mv-ATL*→), an expressive logic to specify strategic abilities in multi-agent systems. It is well known that, for branching-time logics, a general method for model-independent translation from multi-valued to two-valued model checking exists. We show that the method cannot be directly extended to mv-ATL*→. We also propose two ways of overcoming the problem. Firstly, we identify constraints on formulas for which the model-independent translation can be suitably adapted. Secondly, we present a model-dependent reduction that can be applied to all formulas of mv-ATL*→. We show that, in all cases, the complexity of verification increases only linearly when new truth values are added to the evaluation domain. We also consider several examples that show possible applications of mv-ATL*→ and motivate its use for model checking multi-agent systems.

Chat View PDF

On the freeze quantifier in Constraint LTL: Decidability and complexity

2006-10-12

Stéphane Demri , Ranko Lazić , David Nowak

A Hierarchy of Nondeterminism

2022-01-01

Bader Abu Radi , Orna Kupferman , Ofer Leshkowitz

Chat View PDF

Admissibility in Quantitative Graph Games

2016-01-01

Romain Brenguier , Guillermo A. Pérez , Jean-François Raskin +1 more

Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, un- … Admissibility has been studied for games of infinite duration with Boolean objectives. We extend here this study to games of infinite duration with quantitative objectives. First, we show that, un- der the assumption that optimal worst-case and cooperative strategies exist, admissible strategies are guaranteed to exist. Second, we give a characterization of admissible strategies using the no- tion of adversarial and cooperative values of a history, and we characterize the set of outcomes that are compatible with admissible strategies. Finally, we show how these characterizations can be used to design algorithms to decide relevant verification and synthesis problems.

Chat View PDF

Unifying Two Views on Multiple Mean-Payoff Objectives in Markov Decision Processes

2015-07-01

Krishnendu Chatterjee , Zuzana Komárková , Jan Křetínský

We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff … We consider Markov decision processes (MDPs) with multiple limit-average (or mean-payoff) objectives. There exist two different views: (i) ~the expectation semantics, where the goal is to optimize the expected mean-payoff objective, and (ii) ~the satisfaction semantics, where the goal is to maximize the probability of runs such that the mean-payoff value stays above a given vector. We consider optimization with respect to both objectives at once, thus unifying the existing semantics. Precisely, the goal is to optimize the expectation while ensuring the satisfaction constraint. Our problem captures the notion of optimization with respect to strategies that are risk-averse (i.e., Ensure certain probabilistic guarantee). Our main results are as follows: First, we present algorithms for the decision problems, which are always polynomial in the size of the MDP. We also show that an approximation of the Pareto curve can be computed in time polynomial in the size of the MDP, and the approximation factor, but exponential in the number of dimensions. Second, we present a complete characterization of the strategy complexity (in terms of memory bounds and randomization) required to solve our problem.

Chat View PDF

Adding Negative Prices to Priced Timed Games

2014-01-01

Thomas Brihaye , Gilles Geeraerts , Shankara Narayanan Krishna +3 more

Chat View PDF

State of B\"uchi Complementation

2014-12-18

Ming-Hsien Tsai , Seth Fogarty , Moshe Y. Vardi +1 more

Complementation of B\"uchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based … Complementation of B\"uchi automata has been studied for over five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. Regarding the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all of the four approaches to see how they perform in practice. In this paper, we review the four approaches, propose several optimization heuristics, and perform comparative experimentation on four representative constructions that are considered the most efficient in each approach. The experimental results show that (1) the determinization-based Safra-Piterman construction outperforms the other three in producing smaller complements and finishing more tasks in the allocated time and (2) the proposed heuristics substantially improve the Safra-Piterman and the slice-based constructions.

Chat View PDF

Synthesis from LTL Specifications with Mean-Payoff Objectives

2013-01-01

Aaron Bohy , Véronique Bruyère , Emmanuel Filiot +1 more

Chat View PDF

How to Be Both Rich and Happy: Combining Quantitative and Qualitative Strategic Reasoning about Multi-Player Games (Extended Abstract)

2013-02-28

Nils Bulling , Valentin Goranko

We propose a logical framework combining a game-theoretic study of abilities of agents to achieve quantitative objectives in multi-player games by optimizing payoffs or preferences on outcomes with a logical … We propose a logical framework combining a game-theoretic study of abilities of agents to achieve quantitative objectives in multi-player games by optimizing payoffs or preferences on outcomes with a logical analysis of the abilities of players for achieving qualitative objectives of players, i.e., reaching or maintaining game states with desired properties. We enrich concurrent game models with payoffs for the normal form games associated with the states of the model and propose a quantitative extension of the logic ATL* enabling the combination of quantitative and qualitative reasoning.

Chat View PDF