Orna Kupferman
Current Organizations / Institutes
The organizations/institutes from the scholar's latest article
Previous Organizations / Institutes
The organizations / institutes from the scholar's other articles in the past ten years
Research Subjects
Research Interests
Orna Kupferman has a total of 47 co-authors. Here are the top co-authors by number of shared publications:
- Moshe Y. Vardi
Rice University, Houston, TX, USA
9 shared publications - Noam Shenwald
The Hebrew University of Jerusalem
4 shared publications - Ofer Leshkowitz
School of Computer Science and Engineering The Hebrew University of Jerusalem, Israel
4 shared publications - Salomon Sickert
The Hebrew University
4 shared publications - Sarai Sheinvald
Software Engineering, Ort Braude College of Engineering
3 shared publications - Shaull Almagor
Technion
3 shared publications
Latest Publications
- Open Access
- 22 April 2026
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. PP (00985589) , 1-18
Synthesis with Guided Environments
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 real-life applications, in particular when the system serves or directs the environment, it is in the environments interest that the specification is satisfied; hence, it is reasonable to consider satisfaction of the specification only in environments that follow the systems guidance. 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. SGE is thus particularly useful in settings where the system has partial visibility. In software systems, this corresponds to settings that involve hidden user intents, client-local states, or private service policies. 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, SGE for branching-time specifications, and the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.
- 22 April 2026
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Software Engineering
- Vol. PP (00985589) , 1-18
Open AccessSynthesis with Guided Environments
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 real-life applications, in particular when the system serves or directs the environment, it is in the environments interest that the specification is satisfied; hence, it is reasonable to consider satisfaction of the specification only in environments that follow the systems guidance. 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. SGE is thus particularly useful in settings where the system has partial visibility. In software systems, this corresponds to settings that involve hidden user intents, client-local states, or private service policies. 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, SGE for branching-time specifications, and the connection of SGE to synthesis of (possibly distributed) systems with partial visibility.
- 26 October 2025
- Published by Springer Nature
- p. 87-108
Energy Games with Weight Uncertainty
- Open Access
- 1 October 2025
- Published by Elsevier in Information and Computation
- Vol. 307
Monotonicity characterizations of regular languages
- 1 October 2025
- Published by Elsevier in Information and Computation
- Vol. 307
Open AccessMonotonicity characterizations of regular languages
- Open Access
- 20 May 2025
- Published by Springer Nature in Formal Methods in System Design
- Vol. 66 (3) , 376-418
Variable automata over infinite alphabets
Automated reasoning about systems with infinite domains requires an extension of automata, and in particular, finite-word automata, to infinite alphabets. We introduce and study variable finite automata over infinite alphabets (VFAs). VFAs form a natural and simple extension of 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 finite automata, except that some of the transitions are labeled by variables. We compare VFAs with existing formalisms, and study their closure properties and classical decision problems. We further identify and study the deterministic fragment of VFAs (DVFAs). We show that while DVFAs are sufficiently strong to express many interesting properties, they are closed under the Boolean operations, and their nonemptiness and containment problems are decidable. We describe a determinization process for a determinizable subset of VFAs. Moreover, we show that DVFAs have a canonical form, making them a particularly robust model that is easy to reason about and work with. Building on these results, we construct an efficient active learning algorithm for DVFAs, based on the $$L^*$$ learning algorithm for regular languages.- 20 May 2025
- Published by Springer Nature in Formal Methods in System Design
- Vol. 66 (3) , 376-418
Open AccessVariable automata over infinite alphabets
Automated reasoning about systems with infinite domains requires an extension of automata, and in particular, finite-word automata, to infinite alphabets. We introduce and study variable finite automata over infinite alphabets (VFAs). VFAs form a natural and simple extension of 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 finite automata, except that some of the transitions are labeled by variables. We compare VFAs with existing formalisms, and study their closure properties and classical decision problems. We further identify and study the deterministic fragment of VFAs (DVFAs). We show that while DVFAs are sufficiently strong to express many interesting properties, they are closed under the Boolean operations, and their nonemptiness and containment problems are decidable. We describe a determinization process for a determinizable subset of VFAs. Moreover, we show that DVFAs have a canonical form, making them a particularly robust model that is easy to reason about and work with. Building on these results, we construct an efficient active learning algorithm for DVFAs, based on the $$L^*$$ learning algorithm for regular languages. - Open Access
- 1 May 2025
- Published by Springer Nature
- p. 198-216
Synthesis with Guided Environments
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.
- 1 May 2025
- Published by Springer Nature
- p. 198-216
Open AccessSynthesis with Guided Environments
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.
- Open Access
- 1 May 2025
- Published by Springer Nature
- p. 303-322
Non-Zero-Sum Games with Multiple Weighted Objectives
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 $$\alpha $$ of underlying objectives and a weight function $$w: 2^\alpha \rightarrow \mathbb {Z}$$ that maps each subset X of $$\alpha $$ 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.- 1 May 2025
- Published by Springer Nature
- p. 303-322
Open AccessNon-Zero-Sum Games with Multiple Weighted Objectives
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 $$\alpha $$ of underlying objectives and a weight function $$w: 2^\alpha \rightarrow \mathbb {Z}$$ that maps each subset X of $$\alpha $$ 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. - 1 February 2025
- Published by Springer Nature
- p. 67-88
Easy Complementation of History-Deterministic Büchi Automata
- 1 February 2025
- Published by Springer Nature
- p. 67-88
Easy Complementation of History-Deterministic Büchi Automata
- 1 February 2025
- Published by Springer Nature
- p. 3-21
Playing Games on Automata
- Open Access
- 16 April 2024
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 25 (2) , 1-31
The Complexity of LTL Rational Synthesis
In rational synthesis , we automatically construct a reactive system that satisfies its specification in all rational environments, namely environments that have objectives and act to fulfill them. We complete the study of the complexity of LTL rational synthesis, when the objectives are given by formulas in Linear Temporal Logic. Our contribution is threefold. First, we tighten the known upper bounds for settings that were left open in earlier work. Second, our complexity analysis is parametric, and we describe tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components. Third, we generalize the definition of rational synthesis by adding hostile players to the setting and by combining the cooperative and non-cooperative approaches studied in earlier work.
- 16 April 2024
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computational Logic
- Vol. 25 (2) , 1-31
Open AccessThe Complexity of LTL Rational Synthesis
In rational synthesis , we automatically construct a reactive system that satisfies its specification in all rational environments, namely environments that have objectives and act to fulfill them. We complete the study of the complexity of LTL rational synthesis, when the objectives are given by formulas in Linear Temporal Logic. Our contribution is threefold. First, we tighten the known upper bounds for settings that were left open in earlier work. Second, our complexity analysis is parametric, and we describe tight upper and lower bounds in each of the problem parameters: the game graph, the objectives of the system components, and the objectives of the environment components. Third, we generalize the definition of rational synthesis by adding hostile players to the setting and by combining the cooperative and non-cooperative approaches studied in earlier work.