Nir Piterman

KR Conference 2025 Conference Paper

Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis

• Daniel Hausmann
• Shufang Zhu
• Gianmarco Parretti
• Christoph Weinhuber
• Giuseppe De Giacomo
• Nir Piterman

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game. We then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach. We implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.

Highlights Conference 2025 Conference Abstract

Solving Streett and Emerson-Lei Games with Universal Trees

• Nir Piterman

MFCS Conference 2024 Conference Paper

A Direct Translation from LTL with Past to Deterministic Rabin Automata

• Shaun Azzopardi
• David Lidell
• Nir Piterman

We present a translation from linear temporal logic with past to deterministic Rabin automata. The translation is direct in the sense that it does not rely on intermediate non-deterministic automata, and asymptotically optimal, resulting in Rabin automata of doubly exponential size. It is based on two main notions. One is that it is possible to encode the history contained in the prefix of a word, as relevant for the formula under consideration, by performing simple rewrites of the formula itself. As a consequence, a formula involving past operators can (through such rewrites, which involve alternating between weak and strong versions of past operators in the formula’s syntax tree) be correctly evaluated at an arbitrary point in the future without requiring backtracking through the word. The other is that this allows us to generalize to linear temporal logic with past the result that the language of a pure-future formula can be decomposed into a Boolean combination of simpler languages, for which deterministic automata with simple acceptance conditions are easily constructed.

GandALF Workshop 2024 Workshop Paper

Adding Reconfiguration to Zielonka's Asynchronous Automata

• Mathieu Lehaut
• Nir Piterman

We study an extension of Zielonka's (fixed) asynchronous automata called reconfigurable asynchronous automata where processes can dynamically change who they communicate with. We show that reconfigurable asynchronous automata are not more expressive than fixed asynchronous automata by giving translations from one to the other. However, going from reconfigurable to fixed comes at the cost of disseminating communication (and knowledge) to all processes in the system. We then show that this is unavoidable by describing a language accepted by a reconfigurable automaton such that in every equivalent fixed automaton, every process must either be aware of all communication or be irrelevant.

AAMAS Conference 2022 Conference Paper

R-CHECK: A Model Checker for Verifying Reconfigurable MAS

• Yehia Abd Alrahman
• Shaun Azzopardi
• Nir Piterman

Reconfigurable multi-agent systems consist of a set of autonomous agents, with integrated interaction capabilities that feature opportunistic interaction. Agents seemingly reconfigure their interactions interfaces by forming collectives, and interact based on mutual interests. Finding ways to design and analyse the behaviour of these systems is a vigorously pursued research goal. We propose a model checker, named R-CHECK, to allow reasoning about these systems both from an individual- and a system- level. R-CHECK also permits reasoning about interaction protocols and joint missions. R-CHECK supports a high-level input language with symbolic semantics, and provides a modelling convenience for interaction features such as reconfiguration, coalition formation, self-organisation, etc.

KR Conference 2021 Conference Paper

Closed- and Open-world Reasoning in DL-Lite for Cloud Infrastructure Security

• Claudia Cauli
• Magdalena Ortiz
• Nir Piterman

Infrastructure in the cloud is deployed through configuration files, which specify the resources to be created, their settings, and their connectivity. We aim to model infrastructure before deployment and reason about it so that potential vulnerabilities can be discovered and security best practices enforced. Description logics are a good match for such modeling efforts and allow for a succinct and natural description of cloud infrastructure. Their open-world assumption allows capturing the distributed nature of the cloud, where a newly deployed infrastructure could connect to pre-existing resources not necessarily owned by the same user. However, parts of the infrastructure that are fully known need closed-world reasoning, calling for the usage of expressive formalisms, which increase the computational complexity of reasoning. Here, we suggest an extension of DL-LiteF that is tailored for capturing such cloud infrastructure. Our logic allows combining a core part that is completely defined (closed-world) and interacts with a partially known environment (open-world). We show that this extension preserves the first-order rewritability of DL-LiteF for knowledge-base satisfiability and conjunctive query answering. Security properties combine universal and existential reasoning about infrastructure. Thus, we also consider the problem of conjunctive query satisfiability and show that it can be solved in logarithmic space in data complexity.

JAAMAS Journal 2021 Journal Article

Modelling and verification of reconfigurable multi-agent systems

• Yehia Abd Alrahman
• Nir Piterman

Abstract We propose a formalism to model and reason about reconfigurable multi-agent systems. In our formalism, agents interact and communicate in different modes so that they can pursue joint tasks; agents may dynamically synchronize, exchange data, adapt their behaviour, and reconfigure their communication interfaces. Inspired by existing multi-robot systems, we represent a system as a set of agents (each with local state), executing independently and only influence each other by means of message exchange. Agents are able to sense their local states and partially their surroundings. We extend ltl to be able to reason explicitly about the intentions of agents in the interaction and their communication protocols. We also study the complexity of satisfiability and model-checking of this extension.

I&C Journal 2015 Journal Article

The Rabin index of parity games: Its complexity and approximation

• Michael Huth
• Jim Huan-Pu Kuo
• Nir Piterman

ICRA Conference 2013 Conference Paper

Provably correct continuous control for high-level robot behaviors with actions of arbitrary execution durations

• Vasumathi Raman
• Nir Piterman
• Hadas Kress-Gazit

Formal methods have recently been successfully applied to construct verifiable high-level robot control. Most approaches use a discrete abstraction of the underlying continuous domain, and make simplifying assumptions about the physical execution of actions given a discrete implementation. Relaxing these assumptions unearths a number of challenges in the continuous implementation of automatically-synthesized hybrid controllers. This paper describes a controller-synthesis framework that ensures correct continuous behaviors by explicitly modeling the activation and completion of continuous low-level controllers. The synthesized controllers exhibit desired properties like immediate reactiveness to sensor events and guaranteed safety of physical executions. The approach extends to any number of robot actions with arbitrary relative timings.

MFCS Conference 2013 Conference Paper

Synthesis from Temporal Specifications: New Applications in Robotics and Model-Driven Development

• Nir Piterman

Abstract Synthesis from temporal specifications is the automatic production of adaptable plans (or input enabled programs) from high level descriptions. The assumption underlying this form of synthesis is that we have two interacting reactive agents. The first agent is the system for which the plan / program is being designed. The second agent is the environment with which the system interacts. The exact mode of interaction and the knowledge available to each of the agents depends on the application domain.

GandALF Workshop 2013 Workshop Paper

The Rabin index of parity games

• Michael Huth
• Jim Huan-Pu Kuo
• Nir Piterman

We study the descriptive complexity of parity games by taking into account the coloring of their game graphs whilst ignoring their ownership structure. Colored game graphs are identified if they determine the same winning regions and strategies, for *all* ownership structures of nodes. The Rabin index of a parity game is the minimum of the maximal color taken over all equivalent coloring functions. We show that deciding whether the Rabin index is at least k is in PTIME for k=1 but NP-hard for all *fixed* k > 1. We present an EXPTIME algorithm that computes the Rabin index by simplifying its input coloring function. When replacing simple cycle with cycle detection in that algorithm, its output over-approximates the Rabin index in polynomial time. Experimental results show that this approximation yields good values in practice.

TIME Conference 2011 Invited Paper

p-Automata and Obligation Games

• Nir Piterman

We present our automata-based approach to probabilistic verification. This new approach adapts notions and techniques from alternating tree automata to the realm of Markov chains. The resulting p-automata determine languages of Markov chains. In order to determine acceptance of Markov chains by p-automata we develop a new notion of games, which we call \emph{obligation games}. Intuitively, one player commits to achieving a certain probability of winning in the interaction. We survey the initial results regarding obligation games and p-automata. These include algorithms for solving obligation parity games, initial results about the expressive power of p-automata, and the relation between p-automata and pCTL model checking. In particular, these initial foundations show that p-automata enable abstraction-based probabilistic model checking for probabilistic specifications that subsume Markov chains, and LTL and CTL* like logics. Many interesting questions remain open. For example, further algorithmic studies of obligation games, the theory of p-automata, and the usage in practice of p-automata as an abstraction framework for Markov chains.

I&C Journal 2010 Journal Article

Strategy logic

• Krishnendu Chatterjee
• Thomas A. Henzinger
• Nir Piterman

CSL Conference 2006 Conference Paper

Solving Games Without Determinization

• Thomas A. Henzinger
• Nir Piterman

Abstract The synthesis of reactive systems requires the solution of two-player games on graphs with ω -regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton \(\ensuremath {\cal P}\) that is good for solving games with objective \(\ensuremath {\cal P}\). The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.

I&C Journal 2005 Journal Article

Bridging the gap between fair simulation and trace inclusion

• Yonit Kesten
• Nir Piterman
• Amir Pnueli

TCS Journal 2003 Journal Article

From bidirectionality to alternation

• Nir Piterman
• Moshe Y. Vardi

We describe an explicit simulation of 2-way nondeterministic automata by 1-way alternating automata with quadratic blow-up. We first describe the construction for automata on finite words, and extend it to automata on infinite words.

LPAR Conference 2002 Conference Paper

Pushdown Specifications

• Orna Kupferman
• Nir Piterman
• Moshe Y. Vardi

Abstract Traditionally, model checking is applied to finite-state systems and regular specifications. While researchers have successfully extended the applicability of model checking to infinite-state systems, almost all existing work still consider regular specification formalisms. There are, however, many interesting non-regular properties one would like to model check. In this paper we study model checking of pushdown specifications. Our specification formalism is nondeterministic pushdown parity tree automata (PD-NPT). We show that the model-checking problem for regular systems and PD-NPT specifications can be solved in time exponential in the system and the specification. Our model-checking algorithm involves a new solution to the nonemptiness problem of nondeterministic pushdown tree automata, where we improve the best known upper bound from a triple-exponential to a single exponential. We also consider the model-checking problem for context-free systems and PD-NPT specifications and show that it is undecidable.

MFCS Conference 2001 Conference Paper

From Bidirectionality to Alternation

• Nir Piterman
• Moshe Y. Vardi

Abstract We describe an explicit simulation of 2-way nondeterministic automata by 1-way alternating automata with quadratic blow-up. We first describe the construction for automata on finite words, and extend it to automata on infinite words.