The interaction between a system and the components modeling its environment is traditionally modeled by a multi-player game played on a finite graph. In zero-sum games, the players have conflicting objectives, and it is clear that increasing the memory of the environment players can only make it harder for the system to win. In non-zero-sum games, the objectives of the players may overlap. There, typical questions concern the stability of the game and the equilibria the players may reach. In particular, in rational synthesis (RS), the goal is to find an equilibrium that satisfies the objective of the system. We study how the memory of the environment players may affect the existence of an RS solution. As we show, the picture is diverse, even when the objectives of all players are memoryless. On the one hand, when stability amounts to a Nash equilibrium (NE), then increasing the memory of the environment may only help the system to suggest an RS solution. On the other hand, when the notion of stability involves deviations by coalitions of environment players, for example in a strong Nash equilibrium (SNE), then increasing their memory may sometimes enable and sometimes prevent the existence of an RS solution. We study memory bounds for the players, showing that the memory required may be polynomial in an NE-RS solution and exponential in an SNE-RS solution. We also solve the SNE-RS problem, show that it is PSPACE-complete, and relate the differences between NE and SNE with the differences between cooperative and non-cooperative RS. 2012 ACM Subject Classification Theory of computation -> Formal languages and automata theory; Theory of computation -> Semantics and reasoning

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 how its traversal affects the energy level of the system. The system wins if it never runs out of energy. We introduce and study energy games with weight uncertainty (EGWUs), where the exact updates to the energy level are not a-priori known to the system. Instead, an EGWU specifies, for some subsets of edges, upper and lower bounds for their joint weight. EGWUs thus model settings in which there is only an estimation of the effect of some actions or sets of actions on the energy level, for example due to uncertainty about road conditions for an autonomous car or about the location of docking stations for a robot patrolling a warehouse. The system wins an EGWU if it has a strategy to never run out of energy, no matter what the weights are, as long as they respect the bounds. The environment wins if there are weights that respect the bounds with which it can cause the system to run out of energy. Unlike uncertainty about the exact location of the token, which persists during the interaction, the weight of an edge is revealed upon its traversal. The fact the system learns the weights during the interaction makes EGWUs interesting, and we study the memory required to the players, determinacy of the game, and the possibility of coping with uncertainty by a larger initial energy. We give tight complexity bounds to the problems of deciding whether the system or the environment wins, and we study the effect of parameters like the richness of the function estimating the weights, or the distribution of control along the interaction

We introduce and study non-zero-sum multi-player games with weighted multiple objectives. In these games, the objective of each player consists of a set α of underlying objectives and a weight function w: 2^α→ℤ that maps each subset X of α to the utility of the player when exactly all the objectives in X are satisfied. We study the existence and synthesis of stable outcomes with desired utilities for the players. The problem generalizes rational synthesis and enables the synthesis of outcomes that satisfy wellness, fairness, and priority requirements. We study the extension of the game by payments, with which players can incentivize each other to follow strategies that are beneficial for the paying player. We show how such payments can be used in order to repair systems. We study the complexity of the setting for various classes of weight functions. In particular, general weight functions are related to Muller objectives, and the synthesis problem for them is PSPACE-complete. We study non-decreasing, additive, positive, and other classes of weight functions, and the way they affect the memory required for the players and the complexity of the synthesis problem.

The interaction between a system and its environment corresponds to a game in which the system and the environment generate a word over the alphabet of assignments to the input and output signals. The system player wins if the generated word satisfies a desired specification. A correct reactive system has to satisfy its specification in all environments, and thus corresponds to a winning strategy for the system player in the above game. This view is the key to the game-based approach for reactive synthesis. It reduces synthesis to the problem of generating winning strategies in two-player games whose winning conditions are on-going behaviors, which can be specified by automata on infinite words. The paper presents the game-based approach, focusing on ways to cope with the fact that the game cannot be played over nondeterministic automata.

In the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study synthesis with guided environments (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction. The underlying idea in SGE is that in many settings, in particular when the system serves or directs the environment, it is of the environment's interest that the specification is satisfied, and it would follow the guidance of the system. Thus, while the environment is still hostile, in the sense that the system should satisfy the specification no matter how the environment assigns values to the input signals, in SGE the system assigns values to some output signals and guides the environment via programs how to assign values to other output signals. A key issue is that these assignments may depend on input signals that are hidden from the system but are known to the environment, using programs like “copy the value of the hidden input signal x to the output signal y." SGE is thus particularly useful in settings where the system has partial visibility. We solve the problem of SGE, show its superiority with respect to traditional synthesis, and study theoretical aspects of SGE, like the complexity (memory and domain) of programs used by the system, as well as the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.

We introduce and study coverage games - a novel framework for multi-agent planning in settings in which a system operates several agents but do not have full control on them, or interacts with an environment that consists of several agents. The game is played between a coverer, who has a set of objectives, and a disruptor. The coverer operates several agents that interact with the adversarial disruptor. The coverer wins if every objective is satisfied by at least one agent. Otherwise, the disruptor wins. Coverage games thus extend traditional two-player games with multiple objectives by allowing a (possibly dynamic) decomposition of the objectives among the different agents. They have many applications, both in settings where the system is the coverer (e.g., multi-robot surveillance, coverage in multi-threaded systems) and settings where it is the disruptor (e.g., prevention of resource exhaustion, ensuring non-congestion). We study the theoretical properties of coverage games, including determinacy, and the ability to a priori decompose the objectives among the agents. We solve the problems of deciding whether the coverer or the disruptor wins, analyze their tight complexity, and consider useful special cases.

A history deterministic (HD) automaton can successfully resolve its nondeterministic choices in a way that only depends on the past. Formally, an HD automaton has a strategy that maps each finite word to the transition to be taken after the word is read, and following this strategy results in accepting all the words in the language of the automaton. HD automata can replace deterministic automata in several applications, most notably reactive synthesis, and they attract a lot of interest in the research community. In 2015, Kuperberg and Skrzypczak proved that an HD Büchi automaton 𝒜 can be determinized with a quadratic blow-up in the state space. The suggested construction also implicitly induces an HD co-Büchi automaton of linear size that complements 𝒜 . The construction is based on a series of transformations on an HD strategy for 𝒜 , which has two drawbacks. First, the construction is conceptually hard to understand. Second, since the state space of the HD strategy is exponential, so is the runtime of a procedure implementing the construction. In this paper, we describe a direct complementation procedure for HD Büchi automata. Our procedure is based on removal of transitions from 𝒜 itself, which can be done in polynomial time. It results in an HD Büchi automaton equivalent to 𝒜 on top of which we define a complementing HD co-Büchi automaton of linear size. A deterministic equivalent automaton of size quadratic in 𝒜 can then be defined in polynomial time too. We also prove a quadratic lower bound on the size of an HD strategy for HD Büchi automata.

In reactive synthesis, we transform a specification to a system that satisfies the specification in all environments. For specifications in linear-temporal logic, research on bounded synthesis, where the sizes of the system and the environment are bounded, captures realistic settings and has lead to algorithms of improved complexity and implementability. In the game-based approach to synthesis, the system and its environment are modeled by strategies in a two-player game with an.-regular objective, induced by the specification. There, bounded synthesis corresponds to bounding the memory of the strategies of the players. The memory requirement for various objectives has been extensively studied. In particular, researchers have identified positional objectives, where the winning player can follow a memoryless strategy - one that needs no memory. In this work we study bounded synthesis in the game setting. Specifically, we define and study positional-player games, in which one or both players are restricted to memoryless strategies, which correspond to non-intrusive control in various applications. We study positional-player games with Rabin, Streett, and Muller objectives, as well as with weighted multiple Buchi and reachability objectives. Our contribution covers their theoretical properties as well as a complete picture of the complexity of deciding the game in the various settings.

Each language L subset of Sigma & lowast; induces an infinite sequence {Pr(L,n)}infinity n=1, where for all n >= 1, the value Pr(L,n) is an element of [0,1] is the probability of a word of length n to be in L, assuming a uniform distribution on the letters in Sigma. Previous studies of {Pr(L, n)}infinity n=1 for a regular language L, concerned zero-one laws, density, and accumulation points. We study monotonicity of {Pr(L, n)}infinity 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 Land 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 omega is in L. Thus, in the second definition, monotonicity depends not only on the length of w, but also on the words being periodic. We also study the complexity of calculating Pr(L, n) for the various definitions. (c) 2025 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).

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.

Games with multiple objectives arise naturally in synthesis of reactive systems. We study games with weighted multiple objectives. The winning objective in such games consists of a set α of underlying objectives, and a weight function w: 2^α→ I N that maps each subset S of α to a reward earned when exactly all the objectives in S are satisfied. The goal of a player may be to maximize or minimize the reward. As a special case, we obtain games where the goal is to maximize or minimize the number of satisfied objectives, and in particular satisfy them all (a.k.a. generalized conditions). A weight function allows for a much richer reference to the underlying objectives: prioritizing them, referring to desired and less desired combinations, and addressing settings where we cannot expect all sub-specifications to be satisfied together. We focus on settings where the underlying objectives are all Büchi, co-Büchi, reachability, or avoid objectives, and the weight function is non-decreasing (a.k.a. free disposal). For each of the induced classes (that is, type of underlying condition, type of optimization, and type of weight function), we solve the problem of deciding the game and analyze its tight complexity. We also study the tight memory requirements for each of the players. Finally, we consider general weight functions, which make the setting similar to the one of Boolean Muller objectives.

Automated reasoning about systems with infinite domains requires an extension of regular automata to infinite alphabets. Existing formalisms of such automata cope with the infiniteness of the alphabet by adding to the automaton a set of registers or pebbles, or by attributing the alphabet by labels from an auxiliary finite alphabet that is read by an intermediate transducer. These formalisms involve a complicated mechanism on top of the transition function of automata over finite alphabets and are therefore difficult to understand and to work with. We introduce and study variable finite automata over infinite alphabets (VFA). VFA form a natural and simple extension of regular (and ω-regular) automata, in which the alphabet consists of letters as well as variables that range over the infinite alphabet domain. Thus, VFAs have the same structure as regular automata, only that some of the transitions are labeled by variables. We compare VFA with existing formalisms, and study their closure properties and classical decision problems. We consider the settings of both finite and infinite words. In addition, we identify and study the deterministic fragment of VFA. We show that while this fragment is sufficiently strong to express many interesting properties, it is closed under union, intersection, and complementation, and its nonemptiness and containment problems are decidable. Finally, we describe a determinization process for a determinizable subset of VFA.

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.

Classical graph problems are defined with respect to plain graphs, namely vertices connected by possibly weighted edges. On the other hand, model checking studies rich graph structure and semantics, in particular labeled graphs and game graphs, which model involved realistic settings. Extending classical graph problems to graphs with a rich semantics offers an interesting and fresh perspective for classical graph algorithms. In addition, it extends the applicability of graph algorithms to rich settings. In the classical maximum-flow problem, the goal is to find the maximal amount of flow that can be transferred through a network, by directing the flow in each vertex into outgoing edges. The problem has been recently extended to labeled graphs and game graphs. We introduce and study restricted flow games, an extension of the maximum flow-problem to graphs that are both labeled and game graphs. In these games, the edges of the network are labeled by letters over some alphabet, and the vertices are partitioned between two players, the authority and the environment. Each player directs the flow entering her vertices to outgoing edges. The goal of the authority is to maximize the amount of flow that reaches the target along routes that satisfy a given specification - a language over the alphabet of labels. We study several aspects of restricted flow game as well as the complexity of decision problems on them.

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.

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 Buchi, co-Buchi, 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 Buchi and co-Buchi 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.

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.

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.

Nondeterminism models an ability to see the future: An automaton with an infinite look ahead can successfully resolve its nondeterministic choices. An automaton ishistory deterministic(HD) if it can successfully resolve its nondeterministic choices in a way that only depends on the past. Formally, an HD automaton has a strategy that maps each finite word to the transition to be taken after the word is read and following this strategy results in accepting all the words in the language of the automaton. Beyond being theoretically interesting and intriguing, HD automata can replace deterministic automata in several applications, most notably reactive synthesis, and they attract a lot of interest in the research community. The survey describes the development of HD ω-regular automata, relates history determinism to other types of bounded nondeterminism, studies the determinization of HD automata and their succinctness with respect to deterministic ones, and discusses variants, extensions, and open problems around HD automata.