Showing 1–25 of 25 results for author: Piterman, N

A Direct Translation from LTL with Past to Deterministic Rabin Automata

Authors: Shaun Azzopardi, David Lidell, Nir Piterman

Abstract: 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,… ▽ More 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. △ Less

Submitted 29 June, 2024; v1 submitted 2 May, 2024; originally announced May 2024.

Comments: 32 pages. This is the full version of a paper to be published in MFCS'24. Changes since last version: Multiple minor changes addressing reviewer comments. The proof of Lemma 43.2 (previously 34.2) has been made more precise and understandable. Definition 20 (previously 18) has been updated to facilitate making the complexity analysis precise. The appendix is more logically structured

Fair $ω$-Regular Games

Authors: Daniel Hausmann, Nir Piterman, Irmak Sağlam, Anne-Kathrin Schmuck

Abstract: We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip… ▽ More We consider two-player games over finite graphs in which both players are restricted by fairness constraints on their moves. Given a two player game graph $G=(V,E)$ and a set of fair moves $E_f\subseteq E$ a player is said to play "fair" in $G$ if they choose an edge $e \in E_f$ infinitely often whenever the source vertex of $e$ is visited infinitely often. Otherwise, they play "unfair". We equip such games with two $ω$-regular winning conditions $α$ and $β$ deciding the winner of mutually fair and mutually unfair plays, respectively. Whenever one player plays fair and the other plays unfair, the fairly playing player wins the game. The resulting games are called "fair $α/β$ games". We formalize fair $α/β$ games and show that they are determined. For fair parity/parity games, i.e., fair $α/β$ games where $α$ and $β$ are given each by a parity condition over $G$, we provide a polynomial reduction to (normal) parity games via a gadget construction inspired by the reduction of stochastic parity games to parity games. We further give a direct symbolic fixpoint algorithm to solve fair parity/parity games. On a conceptual level, we illustrate the translation between the gadget-based reduction and the direct symbolic algorithm which uncovers the underlying similarities of solution algorithms for fair and stochastic parity games, as well as for the recently considered class of fair games where only one player is restricted by fair moves. △ Less

Submitted 20 October, 2023; originally announced October 2023.

Analyzing Key Users' behavior trends in Volunteer-Based Networks

Authors: Nofar Piterman, Tamar Makov, Michael Fire

Abstract: Online social networks usage has increased significantly in the last decade and continues to grow in popularity. Multiple social platforms use volunteers as a central component. The behavior of volunteers in volunteer-based networks has been studied extensively in recent years. Here, we explore the development of volunteer-based social networks, primarily focusing on their key users' behaviors and… ▽ More Online social networks usage has increased significantly in the last decade and continues to grow in popularity. Multiple social platforms use volunteers as a central component. The behavior of volunteers in volunteer-based networks has been studied extensively in recent years. Here, we explore the development of volunteer-based social networks, primarily focusing on their key users' behaviors and activities. We developed two novel algorithms: the first reveals key user behavior patterns over time; the second utilizes machine learning methods to generate a forecasting model that can predict the future behavior of key users, including whether they will remain active donors or change their behavior to become mainly recipients, and vice-versa. These algorithms allowed us to analyze the factors that significantly influence behavior predictions. To evaluate our algorithms, we utilized data from over 2.4 million users on a peer-to-peer food-sharing online platform. Using our algorithm, we identified four main types of key user behavior patterns that occur over time. Moreover, we succeeded in forecasting future active donor key users and predicting the key users that would change their behavior to donors, with an accuracy of up to 89.6%. These findings provide valuable insights into the behavior of key users in volunteer-based social networks and pave the way for more effective communities-building in the future, while using the potential of machine learning for this goal. △ Less

Submitted 4 October, 2023; originally announced October 2023.

LTL Synthesis on Infinite-State Arenas defined by Programs

Authors: Shaun Azzopardi, Nir Piterman, Gerardo Schneider, Luca di Stefano

Abstract: This paper deals with the problem of automatically and correctly controlling infinite-state reactive programs to achieve LTL goals. Applications include adapting a program to new requirements, or to repair bugs discovered in the original specification or program code. Existing approaches are able to solve this problem for safety and some reachability properties, but require an a priori template of… ▽ More This paper deals with the problem of automatically and correctly controlling infinite-state reactive programs to achieve LTL goals. Applications include adapting a program to new requirements, or to repair bugs discovered in the original specification or program code. Existing approaches are able to solve this problem for safety and some reachability properties, but require an a priori template of the solution for more general properties. Fully automated approaches for full LTL exist, reducing the problem into successive finite LTL reactive synthesis problems in an abstraction-refinement loop. However, they do not terminate when the number of steps to be completed depends on unbounded variables. Our main insight is that safety abstractions of the program are not enough -- fairness properties are also essential to be able to decide many interesting problems, something missed by existing automated approaches. We thus go beyond the state-of-the-art to allow for automated reactive program control for full LTL, with automated discovery of the knowledge, including fairness, of the program needed to determine realisability. We further implement the approach in a tool, with an associated DSL for reactive programs, and illustrate the approach through several case studies. △ Less

Submitted 19 July, 2023; originally announced July 2023.

Correct-by-Construction Design of Contextual Robotic Missions Using Contracts

Authors: Piergiuseppe Mallozzi, Pierluigi Nuzzo, Nir Piterman, Gerardo Schneider, Patrizio Pelliccione

Abstract: Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and execute a robot's high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly… ▽ More Effectively specifying and implementing robotic missions poses a set of challenges to software engineering for robotic systems. These challenges stem from the need to formalize and execute a robot's high-level tasks while considering various application scenarios and conditions, also known as contexts, in real-world operational environments. Writing correct mission specifications that explicitly account for multiple contexts can be tedious and error-prone. Furthermore, as the number of contexts, and consequently the complexity of the specification, increases, generating a correct-by-construction implementation (e.g., by using synthesis methods) can become intractable. A viable approach to address these issues is to decompose the mission specification into smaller, manageable sub-missions, with each sub-mission tailored to a specific context. Nevertheless, this compositional approach introduces its own set of challenges in ensuring the overall mission's correctness. In this paper, we propose a novel compositional framework for specifying and implementing contextual robotic missions using assume-guarantee contracts. The mission specification is structured in a hierarchical and modular fashion, allowing for each sub-mission to be synthesized as an independent robot controller. We address the problem of dynamically switching between sub-mission controllers while ensuring correctness under predefined conditions. △ Less

Submitted 29 December, 2023; v1 submitted 13 June, 2023; originally announced June 2023.

Measuring the Gain of Reconfigurable Communication

Authors: Mathieu Lehaut, Nir Piterman

Abstract: We study the advantages of reconfigurable communication interfaces vs fixed communication interfaces in the context of asynchronous automata. We study the extension of asynchronous (Zielonka) automata with reconfigurable communication interfaces. We show that it is possible to capture languages of automata with reconfigurable communication interfaces by automata with fixed communication interfaces… ▽ More We study the advantages of reconfigurable communication interfaces vs fixed communication interfaces in the context of asynchronous automata. We study the extension of asynchronous (Zielonka) automata with reconfigurable communication interfaces. We show that it is possible to capture languages of automata with reconfigurable communication interfaces by automata with fixed communication interfaces. However, this comes at a cost of disseminating communication (and knowledge) to all agents in a system. Thus, the system is no longer behaving as a distributed system. We then show that this is unavoidable by describing a language in which every agent that uses a fixed communication interface either must be aware of all communication or become irrelevant. △ Less

Submitted 2 May, 2023; originally announced May 2023.

Correct-by-Design Teamwork Plans for Multi-Agent Systems

Authors: Yehia Abd Alrahman, Nir Piterman

Abstract: We propose Teamwork Synthesis, a version of the distributed synthesis problem with application to teamwork multi-agent systems. We reformulate the distributed synthesis question by drop** the fixed interaction architecture among agents as input to the problem. Instead, our synthesis engine tries to realise the goal given the initial specifications; otherwise it automatically introduces minimal i… ▽ More We propose Teamwork Synthesis, a version of the distributed synthesis problem with application to teamwork multi-agent systems. We reformulate the distributed synthesis question by drop** the fixed interaction architecture among agents as input to the problem. Instead, our synthesis engine tries to realise the goal given the initial specifications; otherwise it automatically introduces minimal interactions among agents to ensure distribution. Thus, teamwork synthesis mitigates a key difficulty in deciding algorithmically how agents should interact so that each obtains the required information to fulfil its goal. We show how to apply teamwork synthesis to provide a distributed solution. △ Less

Submitted 12 May, 2023; v1 submitted 3 January, 2023; originally announced January 2023.

A Survey on Satisfiability Checking for the $μ$-Calculus through Tree Automata

Authors: Daniel Hausmann, Nir Piterman

Abstract: Algorithms for model checking and satisfiability of the modal $μ$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of al… ▽ More Algorithms for model checking and satisfiability of the modal $μ$-calculus start by converting formulas to alternating parity tree automata. Thus, model checking is reduced to checking acceptance by tree automata and satisfiability to checking their emptiness. The first reduces directly to the solution of parity games but the second is more complicated. We review the non-emptiness checking of alternating tree automata by a reduction to solving parity games of a certain structure, so-called emptiness games. Since the emptiness problem for alternating tree automata is EXPTIME-complete, the size of these games is exponential in the number of states of the input automaton. We show how the construction of the emptiness games combines a (fixed) structural part with (history-)determinization of parity word automata. For tree automata with certain syntactic structures, simpler methods may be used to handle the treatment of the word automata, which then may be asymptotically smaller than in the general case. These results have direct consequences in satisfiability and validity checking for (various fragments of) the modal $μ$-calculus. △ Less

Submitted 23 August, 2022; v1 submitted 1 July, 2022; originally announced July 2022.

Comments: 28 pages

Actions over Core-closed Knowledge Bases

Authors: Claudia Cauli, Magdalena Ortiz, Nir Piterman

Abstract: We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by… ▽ More We present new results on the application of semantic- and knowledge-based reasoning techniques to the analysis of cloud deployments. In particular, to the security of Infrastructure as Code configuration files, encoded as description logic knowledge bases. We introduce an action language to model mutating actions; that is, actions that change the structural configuration of a given deployment by adding, modifying, or deleting resources. We mainly focus on two problems: the problem of determining whether the execution of an action, no matter the parameters passed to it, will not cause the violation of some security requirement (static verification), and the problem of finding sequences of actions that would lead the deployment to a state where (un)desirable properties are (not) satisfied (plan existence and plan synthesis). For all these problems, we provide definitions, complexity results, and decision procedures. △ Less

Submitted 25 February, 2022; originally announced February 2022.

R-CHECK: A Model Checker for Verifying Reconfigurable MAS

Authors: Yehia Abd Alrahman, Shaun Azzopardi, Nir Piterman

Abstract: 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 mode… ▽ More 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. △ Less

Submitted 25 January, 2022; v1 submitted 17 January, 2022; originally announced January 2022.

Comments: Full version of a tool paper accepted for AAMAS2022

Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue

Authors: Yehia Abd Alrahman, Mauricio Martel, Nir Piterman

Abstract: Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial or… ▽ More Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial order semantics recovers information about the interdependence among the different events for fixed interaction, but still is unable to handle reconfiguration. We introduce glued partial orders as a way to capture reconfiguration. Much like partial orders capture all possible choices for fixed systems, glued partial orders capture all possible choices alongside reconfiguration. We show that a glued partial order is sufficient to correctly capture all partial order computations that differ in forced interleaving due to reconfiguration. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism. △ Less

Submitted 30 July, 2021; originally announced July 2021.

Comments: This work is funded by the ERC consolidator grant D-SynMA (No. 772459) and the Swedish research council grants: SynTM (No.2020-03401) and VR project (No. 2020-04963)

Incorporating Monitors in Reactive Synthesis without Paying the Price

Authors: Shaun Azzopardi, Nir Piterman, Gerardo Schneider

Abstract: Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this p… ▽ More Temporal synthesis attempts to construct reactive programs that satisfy a given declarative (LTL) formula. Practitioners have found it challenging to work exclusively with declarative specifications, and have found languages that combine modelling with declarative specifications more useful. Synthesised controllers may also need to work with pre-existing or manually constructed programs. In this paper we explore an approach that combines synthesis of declarative specifications in the presence of an existing behaviour model as a monitor, with the benefit of not having to reason about the state space of the monitor. We suggest a formal language with automata monitors as non-repeating and repeating triggers for LTL formulas. We use symbolic automata with memory as triggers, resulting in a strictly more expressive and succinct language than existing regular expression triggers. We give a compositional synthesis procedure for this language, where reasoning about the monitor state space is minimal. To show the advantages of our approach we apply it to specifications requiring counting and constraints over arbitrarily long sequence of events, where we can also see the power of parametrisation, easily handled in our approach. We provide a tool to construct controllers (in the form of symbolic automata) for our language. △ Less

Submitted 2 July, 2021; originally announced July 2021.

Modelling and Verification of Reconfigurable Multi-Agent Systems

Authors: 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 (eac… ▽ More 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. △ Less

Submitted 27 April, 2021; v1 submitted 22 April, 2021; originally announced April 2021.

Synthesis of Run-To-Completion Controllers for Discrete Event Systems

Authors: Yehia Abd Alrahman, Victor Braberman, Nicolás D'Ippolito, Nir Piterman, Sebastián Uchitel

Abstract: A controller for a Discrete Event System must achieve its goals despite that its environment being capable of resolving race conditions between controlled and uncontrolled events.Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interru… ▽ More A controller for a Discrete Event System must achieve its goals despite that its environment being capable of resolving race conditions between controlled and uncontrolled events.Assuming that the controller loses all races is sometimes unrealistic. In many cases, a realistic assumption is that the controller sometimes wins races and is fast enough to perform multiple actions without being interrupted. However, in order to model this scenario using control of DES requires introducing foreign assumptions about scheduling, that are hard to figure out correctly. We propose a more balanced control problem, named run-to-completion (RTC), to alleviate this issue. RTC naturally supports an execution assumption in which both the controller and the environment are guaranteed to initiate and perform sequences of actions, without flooding or delaying each other indefinitely. We consider control of DES in the context where specifications are given in the form of linear temporal logic. We formalize the RTC control problem and show how it can be reduced to a standard control problem. △ Less

Submitted 6 September, 2021; v1 submitted 11 September, 2020; originally announced September 2020.

Comments: This work is supported by the following grants: the ERC Consolidator grant D-SynMA (No. 772459), the Marie Skłodowska-Curie BeHAPI (No. 778233), the grants ANPCYT PICT 2018-3835, ANPCYT PICT 2015-1718, CONICET PIP 2014/16 N°11220130100688CO, and UBACYT 20020170100419 BA, , and the Swedish research council grants (No. 2020-04963) and SynTM (No. 2020-03401)

Reconfigurable Interaction for MAS Modelling

Authors: Yehia Abd Alrahman, Giuseppe Perelli, Nir Piterman

Abstract: We propose a formalism to model and reason about multi-agent systems. We allow agents to 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. The formalism defines a local behaviour based on shared variables and a global one based on message passing.… ▽ More We propose a formalism to model and reason about multi-agent systems. We allow agents to 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. The formalism defines a local behaviour based on shared variables and a global one based on message passing. We extend LTL to be able to reason explicitly about the intentions of the different agents and their interaction protocols. We also study the complexity of satisfiability and model-checking of this extension. △ Less

Submitted 19 February, 2020; v1 submitted 25 June, 2019; originally announced June 2019.

Comments: This is a final and revised version. This research is funded by the ERC consolidator grant D-SynMA under the European Union's Horizon 2020 research and innovation programme (grant agreement No 772459)

Environmentally-friendly GR(1) Synthesis

Authors: Rupak Majumdar, Nir Piterman, Anne-Kathrin Schmuck

Abstract: Many problems in reactive synthesis are stated using two formulas ---an environment assumption and a system guarantee--- and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally cor… ▽ More Many problems in reactive synthesis are stated using two formulas ---an environment assumption and a system guarantee--- and ask for an implementation that satisfies the guarantee in environments that satisfy their assumption. Reactive synthesis tools often produce strategies that formally satisfy such specifications by actively preventing an environment assumption from holding. While formally correct, such strategies do not capture the intention of the designer. We introduce an additional requirement in reactive synthesis, non-conflictingness, which asks that a system strategy should always allow the environment to fulfill its liveness requirements. We give an algorithm for solving GR(1) synthesis that produces non-conflicting strategies. Our algorithm is given by a 4-nested fixed point in the $μ$-calculus, in contrast to the usual 3-nested fixed point for GR(1). Our algorithm ensures that, in every environment that satisfies its assumptions on its own, traces of the resulting implementation satisfy both the assumptions and the guarantees. In addition, the asymptotic complexity of our algorithm is the same as that of the usual GR(1) solution. We have implemented our algorithm and show how its performance compares to the usual GR(1) synthesis algorithm. △ Less

Submitted 14 February, 2019; originally announced February 2019.

Comments: Full version of the TACAS'19 paper with the same title

Coverability: Realizability Lower Bounds

Authors: Krishnendu Chatterjee, Nir Piterman

Abstract: We introduce the problem of temporal coverability for realizability and synthesis. Namely, given a language of words that must be covered by a produced system, how to automatically produce such a system. We consider the case of coverability with no further specifications, where we have to show that the nondeterminism of the produced system is sufficient to produce all the words required in the out… ▽ More We introduce the problem of temporal coverability for realizability and synthesis. Namely, given a language of words that must be covered by a produced system, how to automatically produce such a system. We consider the case of coverability with no further specifications, where we have to show that the nondeterminism of the produced system is sufficient to produce all the words required in the output language. We show a counting argument on a deterministic automaton representing the language to be covered that allows to produce such a system. We then turn to the case of coverability with additional specification and give a precondition for the existence of a system that produces all required words and at the same time produces only computations satisfying the additional correctness criterion. We combine our counting argument on the deterministic automaton for the language to be covered with a ranking on the deterministic Büchi automaton for the correctness criterion. One of the major issues with practical realizability is the interaction between environment assumptions and system guarantees. In many cases, synthesis produces systems that are vacuous and concentrate on forcing the environment to falsify its assumptions instead of fulfilling their guarantees. Coverability offers an alternative approach to tackle this problem. △ Less

Submitted 10 April, 2018; originally announced April 2018.

Combinations of Qualitative Winning for Stochastic Parity Games

Authors: Krishnendu Chatterjee, Nir Piterman

Abstract: We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths must satisfy the condition, almost-sure winning, which requires the condition is satisfied with probability~1, and limit-sure winning, which requires the condition is satisfied with probability arbitrarily close to~1… ▽ More We study Markov decision processes and turn-based stochastic games with parity conditions. There are three qualitative winning criteria, namely, sure winning, which requires all paths must satisfy the condition, almost-sure winning, which requires the condition is satisfied with probability~1, and limit-sure winning, which requires the condition is satisfied with probability arbitrarily close to~1. We study the combination of these criteria for parity conditions, e.g., there are two parity conditions one of which must be won surely, and the other almost-surely. The problem has been studied recently by Berthon et.~al for MDPs with combination of sure and almost-sure winning, under infinite-memory strategies, and the problem has been established to be in NP $\cap$ coNP. Even in MDPs there is a difference between finite-memory and infinite-memory strategies. Our main results for combination of sure and almost-sure winning are as follows: (a)~we show that for MDPs with finite-memory strategies the problem lie in NP $\cap$ coNP; (b)~we show that for turn-based stochastic games the problem is coNP-complete, both for finite-memory and infinite-memory strategies; and (c)~we present algorithmic results for the finite-memory case, both for MDPs and turn-based stochastic games, by reduction to non-stochastic parity games. In addition we show that all the above results also carry over to combination of sure and limit-sure winning, and results for all other combinations can be derived from existing results in the literature. Thus we present a complete picture for the study of combinations of qualitative winning criteria for parity conditions in MDPs and turn-based stochastic games. △ Less

Submitted 10 April, 2018; originally announced April 2018.

T2: Temporal Property Verification

Authors: Marc Brockschmidt, Byron Cook, Samin Ishtiaq, Heidy Khlaaf, Nir Piterman

Abstract: We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architectur… ▽ More We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving techniques and to handle a general class of user-provided liveness and safety properties. Input can be provided in a native format and in C, via the support of the LLVM compiler framework. We briefly discuss T2's architecture, its underlying techniques, and conclude with an experimental illustration of its competitiveness and directions for future extensions. △ Less

Submitted 6 January, 2016; v1 submitted 29 December, 2015; originally announced December 2015.

Comments: Full version of TACAS'16 tool paper

Synthesising Executable Gene Regulatory Networks from Single-cell Gene Expression Data

Authors: Jasmin Fisher, Ali Sinan Köksal, Nir Piterman, Steven Woodhouse

Abstract: Recent experimental advances in biology allow researchers to obtain gene expression profiles at single-cell resolution over hundreds, or even thousands of cells at once. These single-cell measurements provide snapshots of the states of the cells that make up a tissue, instead of the population-level averages provided by conventional high-throughput experiments. This new data therefore provides an… ▽ More Recent experimental advances in biology allow researchers to obtain gene expression profiles at single-cell resolution over hundreds, or even thousands of cells at once. These single-cell measurements provide snapshots of the states of the cells that make up a tissue, instead of the population-level averages provided by conventional high-throughput experiments. This new data therefore provides an exciting opportunity for computational modelling. In this paper we introduce the idea of viewing single-cell gene expression profiles as states of an asynchronous Boolean network, and frame model inference as the problem of reconstructing a Boolean network from its state space. We then give a scalable algorithm to solve this synthesis problem. We apply our technique to both simulated and real data. We first apply our technique to data simulated from a well established model of common myeloid progenitor differentiation. We show that our technique is able to recover the original Boolean network rules. We then apply our technique to a large dataset taken during embryonic development containing thousands of cell measurements. Our technique synthesises matching Boolean networks, and analysis of these models yields new predictions about blood development which our experimental collaborators were able to verify. △ Less

Submitted 17 January, 2018; v1 submitted 19 May, 2015; originally announced May 2015.

Comments: Final published version to appear in Computer Aided Verification (CAV), Springer, July 2015

Fatal Attractors in Parity Games: Building Blocks for Partial Solvers

Authors: Michael Huth, Jim Huan-Pu Kuo, Nir Piterman

Abstract: Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion.… ▽ More Attractors in parity games are a technical device for solving "alternating" reachability of given node sets. A well known solver of parity games - Zielonka's algorithm - uses such attractor computations recursively. We here propose new forms of attractors that are monotone in that they are aware of specific static patterns of colors encountered in reaching a given node set in alternating fashion. Then we demonstrate how these new forms of attractors can be embedded within greatest fixed-point computations to design solvers of parity games that run in polynomial time but are partial in that they may not decide the winning status of all nodes in the input game. Experimental results show that our partial solvers completely solve benchmarks that were constructed to challenge existing full solvers. Our partial solvers also have encouraging run times in practice. For one partial solver we prove that its run-time is at most cubic in the number of nodes in the parity game, that its output game is independent of the order in which monotone attractors are computed, and that it solves all Buechi games and weak games. We then define and study a transformation that converts partial solvers into more precise partial solvers, and we prove that this transformation is sound under very reasonable conditions on the input partial solvers. Noting that one of our partial solvers meets these conditions, we apply its transformation on 1.6 million randomly generated games and so experimentally validate that the transformation can be very effective in increasing the precision of partial solvers. △ Less

Submitted 19 May, 2014; v1 submitted 2 May, 2014; originally announced May 2014.

The Rabin index of parity games

Authors: Michael Huth, Jim Huan-Pu Kuo, Nir Piterman

Abstract: 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.… ▽ More 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. △ Less

Submitted 16 July, 2013; originally announced July 2013.

Comments: In Proceedings GandALF 2013, arXiv:1307.4162

Journal ref: EPTCS 119, 2013, pp. 35-49

Obligation Blackwell Games and p-Automata

Authors: Krishnendu Chatterjee, Nir Piterman

Abstract: We recently introduced p-automata, automata that read discrete-time Markov chains. We used turn-based stochastic parity games to define acceptance of Markov chains by a subclass of p-automata. Definition of acceptance required a cumbersome and complicated reduction to a series of turn-based stochastic parity games. The reduction could not support acceptance by general p-automata, which was left un… ▽ More We recently introduced p-automata, automata that read discrete-time Markov chains. We used turn-based stochastic parity games to define acceptance of Markov chains by a subclass of p-automata. Definition of acceptance required a cumbersome and complicated reduction to a series of turn-based stochastic parity games. The reduction could not support acceptance by general p-automata, which was left undefined as there was no notion of games that supported it. Here we generalize two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1. One cannot define value in obligation games by the standard mechanism of considering the measure of winning paths on a Markov chain and taking the supremum of the infimum of all strategies. Mainly because obligations need definition even for Markov chains and the nature of obligations has the flavor of an infinite nesting of supremum and infimum operators. We define value via a reduction to turn-based games similar to Martin's proof of determinacy of Blackwell games with Borel objectives. Based on this definition, we show that games are determined. We show that for Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations there exists an alternative and simpler characterization of the value function. Based on this simpler definition we give an exponential time algorithm to analyze finite turn-based stochastic parity games with obligations. Finally, we show that obligation games provide the necessary framework for reasoning about p-automata and that they generalize the previous definition. △ Less

Submitted 3 November, 2013; v1 submitted 22 June, 2012; originally announced June 2012.

Algorithms for Büchi Games

Authors: Krishnendu Chatterjee, Thomas A. Henzinger, Nir Piterman

Abstract: The classical algorithm for solving Büchi games requires time $O(n\cdot m)$ for game graphs with $n$ states and $m$ edges. For game graphs with constant outdegree, the best known algorithm has running time $O(n^2/\log n)$. We present two new algorithms for Büchi games. First, we give an algorithm that performs at most $O(m)$ more work than the classical algorithm, but runs in time O(n) on infini… ▽ More The classical algorithm for solving Büchi games requires time $O(n\cdot m)$ for game graphs with $n$ states and $m$ edges. For game graphs with constant outdegree, the best known algorithm has running time $O(n^2/\log n)$. We present two new algorithms for Büchi games. First, we give an algorithm that performs at most $O(m)$ more work than the classical algorithm, but runs in time O(n) on infinitely many graphs of constant outdegree on which the classical algorithm requires time $O(n^2)$. Second, we give an algorithm with running time $O(n\cdot m\cdot\logδ(n)/\log n)$, where $1\leδ(n)\le n$ is the outdegree of the game graph. Note that this algorithm performs asymptotically better than the classical algorithm if $δ(n)=O(\log n)$. △ Less

Submitted 16 May, 2008; originally announced May 2008.

Comments: 11 Pages, Published in GDV 06 (Games in Design and Verification)

From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata

Authors: Nir Piterman

Abstract: 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 bo… ▽ More 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). △ Less

Submitted 14 August, 2007; v1 submitted 15 May, 2007; originally announced May 2007.

Comments: 21 pages. To appear in Logical Methods in Computer Science (LMCS)

ACM Class: F.1.1; F.4.3

Journal ref: Logical Methods in Computer Science, Volume 3, Issue 3 (August 14, 2007) lmcs:1199