Sasha Rubin

I&C Journal 2025 Journal Article

ltl synthesis under environment specifications for reachability and safety properties

• Benjamin Aminof
• Giuseppe De Giacomo
• Antonio Di Stasio
• Hugo Francon
• Sasha Rubin
• Shufang Zhu

In this paper, we study ltl f synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

KR Conference 2025 Conference Paper

LTL Synthesis Under Multi-Agent Environment Assumptions

• Benjamin Aminof
• Giuseppe De Giacomo
• Giuseppe Perelli
• Sasha Rubin

We investigate LTL synthesis under structured assumptions about the environment. In our setting, the environment is viewed by the protagonist as a collection of peer agents acting together in a shared world. In contrast to the symmetrical frameworks typically studied in multi-agent systems, we take a strikingly asymmetric first-person perspective in which the protagonist ascribes a specification to each of its peer agents and the world, capturing its understanding of their possible strategies. We show that in this setting, LTL synthesis has the same computational complexity as standard LTL synthesis, i. e. , 2EXPTIME-complete. We establish this via a sophisticated, yet fully implementable, argument that builds on the notion of traces compatible with strategies: we use the fact that if the basic specification of the world and of each agent is given in LTL then the sets of traces compatible with the strategies describing the behaviors of the agents are omega-regular. This enables the use of word-automata rather than the more complicated tree-automata.

IJCAI Conference 2025 Conference Paper

LTLf+ and PPLTL+: Extending LTLf and PPLTL to Infinite Traces

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin
• Moshe Y. Vardi

We study two logics, LTLf+ and PPLTL+, to express properties of infinite traces, that are based on the linear-time temporal logics LTLf and PPLTL on finite traces. LTLf+/PPLTL+ use levels of Manna and Pnueli’s LTL safety-progress hierarchy, and thus have the same expressive power as LTL. However, they also retain a crucial characteristic of reactive synthesis for the base logics: the game arena for strategy extraction can be derived from deterministic finite automata (DFA). Consequently, these logics circumvent the notorious difficulties associated with determinizing infinite trace automata, typical of LTL synthesis. We present optimal DFA-based technique for solving reactive synthesis for LTLf+ and PPLTL+. Additionally, we adapt these algorithms to optimally solve satisfiability and model-checking for these two logics.

IJCAI Conference 2025 Conference Paper

Most General Explanations of Tree Ensembles

• Yacine Izza
• Akexey Ignatiev
• Sasha Rubin
• Joao Marques-Silva
• Peter J. Stuckey

Explainable Artificial Intelligence (XAI) is critical for attaining trust in the operation of AI systems. A key question of an AI system is ``why was this decision made this way''. Formal approaches to XAI use a formal model of the AI system to identify abductive explanations. While abductive explanations may be applicable to a large number of inputs sharing the same concrete values, more general explanations may be preferred for numeric inputs. So-called inflated abductive explanations give intervals for each feature ensuring that any input whose values fall withing these intervals is still guaranteed to make the same prediction. Inflated explanations cover a larger portion of the input space, and hence are deemed more general explanations. But there can be many (inflated) abductive explanations for an instance. Which is the best? In this paper, we show how to find a most general abductive explanation for an AI decision. This explanation covers as much of the input space as possible, while still being a correct formal explanation of the model's behaviour. Given that we only want to give a human one explanation for a decision, the most general explanation gives us the explanation with the broadest applicability, and hence the one most likely to seem sensible.

IJCAI Conference 2024 Conference Paper

Effective Approach to LTLf Best-Effort Synthesis in Multi-Tier Environments

• Benjamin Aminof
• Giuseppe De Giacomo
• Gianmarco Parretti
• Sasha Rubin

We consider an agent acting in a complex environment modeled through a multi-tiered specification, in which each tier adds nondeterminism in the environment response to the agent actions. In this setting, we devise an effective approach to best-effort synthesis, i. e. , synthesizing agent strategies that win against a maximal set of possible environment responses in each tier. We do this in a setting where both the multi-tier environment and agent goal are specified in the linear temporal logic on finite traces (LTLf). While theoretical solution techniques based on automata on infinite trees have been developed previously, we completely side-step them here and focus on a DFA-based game-theoretic technique, which can be effectively implemented symbolically. Specifically, we present a provably correct algorithm that is based on solving separately DFA-based games for each tier and then combining the obtained solutions on-the-fly. This algorithm is linear, as opposed to being exponential, in the number of tiers and thus, it can graciously handle multi-tier environments formed of several tiers.

ICAPS Conference 2024 Conference Paper

Planning with Object Creation

• Augusto B. Corrêa
• Giuseppe De Giacomo
• Malte Helmert
• Sasha Rubin

Classical planning problems are defined using some specification language, such as PDDL. The domain expert defines action schemas, objects, the initial state, and the goal. One key aspect of PDDL is that the set of objects cannot be modified during plan execution. While this is fine in many domains, sometimes it makes modeling more complicated. This may impact the performance of planners, and it requires the domain expert to bound the number of required objects beforehand, which can be a challenge. We introduce an extension to the classical planning formalism, where action effects can create and remove objects. This problem is semi-decidable, but it becomes decidable if we can bound the number of objects in any given state, even though the state space is still infinite. On the practical side, we extend the Powerlifted planning system to support this PDDL extension. Our results show that this extension improves the performance of Powerlifted while supporting more natural PDDL models.

KR Conference 2024 Conference Paper

Probabilistic Synthesis and Verification for LTL on Finite Traces

• Benjamin Aminof
• Linus Cooper
• Sasha Rubin
• Moshe Y. Vardi
• Florian Zuleger

We study synthesis and verification of probabilistic models and specifications over finite traces. Probabilistic models are formalized in this work as Markov Chains and Markov Decisions Processes. Motivated by the recent attention given to, and importance of, finite-trace specifications in AI, we use linear-temporal logic on finite traces as a specification formalism for properties of traces with finite but unbounded time horizons. Since there is no bound on the time horizon, our Markov chains generate infinite traces, and we consider two possible semantics: “existential (resp. universal) prefix- semantics” which says that the finite-trace property holds on some (resp. every) finite prefix of the trace. For both types of semantics, we study two computational problems: the verification problem — “does a given Markov chain satisfy the specification with probability one? ”; and the synthesis problem — “find a strategy (if there is one) that ensures the Markov decision process satisfies the specification with probability one”. We provide optimal algorithms that follow an automata-theoretic approach, and prove that the complexity of the synthesis problem is 2EXPTIME-complete for both semantics, and that for the verification problem it is PSPACE-complete for the universal-prefix semantics, but EXPSPACE-complete for the existential-prefix semantics.

KR Conference 2024 Conference Paper

Proper Linear-time Specifications of Environment Behaviors in Nondeterministic Planning and Reactive Synthesis

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin
• Florian Zuleger

To help it achieve its goal, an agent exploits assumptions it has about the behavior of its environment. The common view in planning and reactive synthesis is that such assumptions are sets of traces. This trace-centric view has the advantage of having well-understood specification formalisms, such as linear-time temporal logic. An alternative view, that we have promoted as being conceptually superior, is strategy-centric: assumptions are non-empty sets of environment strategies. In this work we relate these views and show that the strategy-centric view is a refinement of the trace-centric view. We thus address the following fundamental question: when should a set of traces be considered an assumption that the agent has about the environment's behavior? Our answer is in terms of coverability: every trace in the set should be consistent with some environment strategy that enforces it. We call such sets ``proper environment specifications''. Typical examples are given by (the traces consistent with a given) planning domain, and fairness constraints, but not arbitrary trace constraints. We provide an algorithm that, given a specification in linear-time temporal logic (LTL) decides whether or not it is a proper environment specification. Furthermore, we show that every set of traces has a ``proper environment core'', which excludes traces that the agent can ignore when devising its plan. We provide an algorithm for computing a representation of the core of an LTL formula, and prove that the core of an LTL-definable property is itself LTL-definable.

LAMAS&SR Workshop 2023 Workshop Paper

LTLf Synthesis Under Environment Specifications for Reachability and Safety Properties

• Benjamin Aminof
• Giuseppe De Giacomo
• Antonio Di Stasio
• Hugo Francon
• Sasha Rubin
• Shufang Zhu

In this paper, we study LTLf synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. All these algorithms adopt some common building blocks, though combining them in different ways. While some cases are already studied in literature others are studied here for the first time.

AAAI Conference 2023 Conference Paper

Reactive Synthesis of Dominant Strategies

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin

We study the synthesis under environment specifications problem for LTL/LTLf which, in particular, generalizes FOND (strong) planning with these temporal goals. We consider the case where the agent cannot enforce its goal --- for which the argument for using best-effort strategies has been made --- and study the intermediate ground, between enforcing and best-effort strategies, of dominant strategies. Intuitively, such strategies achieve the goal against any environment for which it is achievable. We show that dominant strategies may exist when enforcing ones do not, while still sharing with the latter many desirable properties such as being interchangeable with each other, and being monotone with respect to tightening of environment specifications. We give necessary and sufficient conditions for the existence of dominant strategies, and show that deciding if they exist is 2EXPTIME-complete --- the same as for enforcing strategies. Finally, we give a uniform, optimal, game-theoretic algorithm for simultaneously solving the three synthesis problems of enforcing, dominant, and best-effort strategies.

EUMAS Conference 2023 Conference Paper

sc ltl f Synthesis Under Environment Specifications for Reachability and Safety Properties

• Benjamin Aminof
• Giuseppe De Giacomo
• Antonio Di Stasio 0001
• Hugo Francon
• Sasha Rubin
• Shufang Zhu 0001

Abstract In this paper, we study \({\textsc {ltl}}_f\) synthesis under environment specifications for arbitrary reachability and safety properties. We consider both kinds of properties for both agent tasks and environment specifications, providing a complete landscape of synthesis algorithms. For each case, we devise a specific algorithm (optimal wrt complexity of the problem) and prove its correctness. The algorithms combine common building blocks in different ways. While some cases are already studied in literature others are studied here for the first time.

IJCAI Conference 2022 Conference Paper

Beyond Strong-Cyclic: Doing Your Best in Stochastic Environments

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin
• Florian Zuleger

``Strong-cyclic policies" were introduced to formalize trial-and-error strategies and are known to work in Markovian stochastic domains, i. e. , they guarantee that the goal is reached with probability 1. We introduce ``best-effort" policies for (not necessarily Markovian) stochastic domains. These generalize strong-cyclic policies by taking advantage of stochasticity even if the goal cannot be reached with probability 1. We compare such policies with optimal policies, i. e. , policies that maximize the probability that the goal is achieved, and show that optimal policies are best-effort, but that the converse is false in general. With this framework at hand, we revisit the foundational problem of what it means to plan in nondeterministic domains when the nondeterminism has a stochastic nature. We show that one can view a nondeterministic planning domain as a representation of infinitely many stochastic domains with the same support but different probabilities, and that for temporally extended goals expressed in LTL/LTLf a finite-state best-effort policy in one of these domains is best-effort in each of the domains. In particular, this gives an approach for finding such policies that reduces to solving finite-state MDPs with LTL/LTLf goals. All this shows that ``best-effort" policies are robust to changes in the probabilities, as long as the support is unchanged.

AAAI Conference 2022 Conference Paper

Formula Synthesis in Propositional Dynamic Logic with Shuffle

• Sophie Pinchinat
• Sasha Rubin
• François Schwarzentruber

We introduce the formula-synthesis problem for Propositional Dynamic Logic with Shuffle (PDL|| ). This problem, which generalises the model-checking problem againsts PDL|| is the following: given a finite transition system and a regular term-grammar that generates (possibly infinitely many) PDL|| formulas, find a formula generated by the grammar that is true in the structure (or return that there is none). We prove that the problem is undecidable in general, but add certain restrictions on the input structure or on the input grammar to yield decidability. In particular, we prove that (1) if the grammar only generates formulas in PDL (without shuffle), then the problem is EXPTIME-complete, and a further restriction to linear grammars is PSPACE-complete, and a further restriction to non-recursive grammars is NP-complete, and (2) if one restricts the input structure to have only simple paths then the problem is in 2-EXPTIME. This work is motivated by and opens up connections to other forms of synthesis from hierarchical descriptions, including HTN problems in Planning and Attack-tree Synthesis problems in Security.

LAMAS&SR Workshop 2022 Workshop Paper

Formula synthesis in propositional dynamic logic with shuffle

• Sophie Pinchinat
• Sasha Rubin
• Francois Schwarzentruber

KR Conference 2022 Conference Paper

Public and Private Affairs in Strategic Reasoning

• Nathanaël Fijalkow
• Bastien Maubert
• Aniello Murano
• Sasha Rubin
• Moshe Vardi

Do agents know each others’ strategies? In multi-process software construction, each process has access to the processes already constructed; but in typical human-robot interactions, a human may not announce its strategy to the robot (indeed, the human may not even know their own strategy). This question has often been overlooked when modeling and reasoning about multi-agent systems. In this work, we study how it impacts strategic reasoning. To do so we consider Strategy Logic (SL), a well-established and highly expressive logic for strategic reasoning. Its usual semantics, which we call “white-box semantics”, models systems in which agents “broadcast” their strategies. By adding imperfect information to the evaluation games for the usual semantics, we obtain a new semantics called “black-box semantics”, in which agents keep their strategies private. We consider the model-checking problem and show that the black-box semantics has much lower complexity than white-box semantics for an important fragment of Strategy Logic.

Highlights Conference 2022 Conference Abstract

Stochastic Best-Effort Synthesis

• Sasha Rubin

In this talk I will introduce a new class of strategies for solving synthesis in non-Markovian stochastic domains with linear-time goals called 'stochastic best-effort' (SBE) strategies. A SBE strategy is one that, from every history, ensures the goal is satisfied with probability 1 if this is possible, and otherwise ensures the goal is satisfied with positive probability if this is possible. Like optimal strategies, SBE strategies take advantage of stochasticity even if the goal cannot be enforced with probability 1 from the initial state. However, in contrast to optimal strategies, SBE strategies always exist. Moreover, like strategies that enforce the goal with probability 1, SBE strategies do not depend on the precise probabilities (under some reasonable and necessary conditions). At the end of the talk, I will discuss how these results shed light on the nature of nondeterministic planning in AI. This is joint work with Benjamin Aminof, Giuseppe De Giacomo, and Florian Zuleger.

AAAI Conference 2022 Conference Paper

Sufficient Reasons for Classifier Decisions in the Presence of Domain Constraints

• Niku Gorji
• Sasha Rubin

Recent work has unveiled a theory for reasoning about the decisions made by binary classifiers: a classifier describes a Boolean function, and the reasons behind an instance being classified as positive are the prime-implicants of the function that are satisfied by the instance. One drawback of these works is that they do not explicitly treat scenarios where the underlying data is known to be constrained, e. g. , certain combinations of features may not exist, may not be observable, or may be required to be disregarded. We propose a more general theory, also based on prime-implicants, tailored to taking constraints into account. The main idea is to view classifiers as describing partial Boolean functions that are undefined on instances that do not satisfy the constraints. We prove that this simple idea results in more parsimonious reasons. That is, not taking constraints into account (e. g. , ignoring, or taking them as negative instances) results in reasons that are subsumed by reasons that do take constraints into account. We illustrate this improved succinctness on synthetic classifiers and classifiers learnt from real data.

AIJ Journal 2022 Journal Article

Verification of agent navigation in partially-known environments

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin
• Florian Zuleger

This paper establishes a framework based on logic and automata theory in which to model and automatically verify systems of multiple mobile agents moving in environments with partially-known topologies, i. e. , ones which are not completely known at design time. Examples include physical agents designed to be used in many spatial environments and not tailored for a specific one, robots in environments not reachable by humans, and software exploring partially-mapped networks. We model spatial environments as graphs whose edges are labelled with directions. We model agents as finite-state machines that move on the graphs by issuing commands of the form “go in direction X”, that can communicate their internal state to other agents, and that can sense agent positions (including current and visited positions). We treat the incomplete information about the spatial environment by studying the decision problem that asks whether a given collection of agents achieve their tasks on all graphs from a class of graphs — this is called the parameterised verification problem. The framework also introduces a new logical language based on Linear Temporal Logic that is tailored for expressing agent navigation tasks in such environments. Although the parameterised verification problem is undecidable, we identify two key dimensions that need to be limited in order to regain decidability, namely, the set of graph-environments and the amount of sensing and communication between agents. In particular, one should limit the families of graphs to exclude grids, and there should be a bound on the number of times an agent senses the position of another agent or communicates its own state to another agent. We prove that dropping either of these assumptions results in undecidability, even for agents with severe restrictions on their abilities (e. g. , with very limited sensing abilities and no communication abilities). The importance of this work is that a) it provides a general computational model for mobile multi-agent systems in environments with partially-known topologies, b) it identifies, for the first time, the precise causes of undecidability of these systems and presents minimal restrictions to alleviate this problem, and c) it provides a generic sound and complete procedure for solving the parameterised verification problem over a broad range of spatial-environments and for agents with very powerful sensing and communication abilities.

IJCAI Conference 2021 Conference Paper

Best-Effort Synthesis: Doing Your Best Is Not Harder Than Giving Up

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin

We study best-effort synthesis under environment assumptions specified in LTL, and show that this problem has exactly the same computational complexity of standard LTL synthesis: 2EXPTIME-complete. We provide optimal algorithms for computing best-effort strategies, both in the case of LTL over infinite traces and LTL over finite traces (i. e. , LTLf). The latter are particularly well suited for implementation.

IJCAI Conference 2021 Conference Paper

Reasoning About Agents That May Know Other Agents’ Strategies

• Francesco Belardinelli
• Sophia Knight
• Alessio Lomuscio
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study the semantics of knowledge in strategic reasoning. Most existing works either implicitly assume that agents do not know one another’s strategies, or that all strategies are known to all; and some works present inconsistent mixes of both features. We put forward a novel semantics for Strategy Logic with Knowledge that cleanly models whose strategies each agent knows. We study how adopting this semantics impacts agents’ knowledge and strategic ability, as well as the complexity of the model-checking problem.

KR Conference 2021 Conference Paper

Synthesizing Best-effort Strategies under Multiple Environment Specifications

• Benjamin Aminof
• Giuseppe De Giacomo
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We formally introduce and solve the synthesis problem for LTL goals in the case of multiple, even contradicting, assumptions about the environment. Our solution concept is based on ``best-effort strategies'' which are agent plans that, for each of the environment specifications individually, achieve the agent goal against a maximal set of environments satisfying that specification. By means of a novel automata theoretic characterization we demonstrate that this best-effort synthesis for multiple environments is 2ExpTime-complete, i. e. , no harder than plain LTL synthesis. We study an important case in which the environment specifications are increasingly indeterminate, and show that as in the case of a single environment, best-effort strategies always exist for this setting. Moreover, we show that in this setting the set of solutions are exactly the strategies formed as follows: amongst the best-effort agent strategies for ɸ under the environment specification E1, find those that do a best-effort for ɸ under (the more indeterminate) environment specification E2, and amongst those find those that do a best-effort for ɸ under the environment specification E3, etc.

KR Conference 2020 Conference Paper

High-level Programming via Generalized Planning and LTL Synthesis

• Blai Bonet
• Giuseppe De Giacomo
• Hector Geffner
• Fabio Patrizi
• Sasha Rubin

We look at program synthesis where the aim is to automatically synthesize a controller that operates on data structures and from which a concrete program can be easily derived. We do not aim at a fully-automatic process or tool that produces a program meeting a given specification of the program’s behaviour. Rather, we aim at the design of a clear and well-founded approach for supporting programmers at the design and implementation phases. Concretely, we first show that a program synthesis task can be modeled as a generalized planning problem. This is done at an abstraction level where the involved data structures are seen as black-boxes that can be interfaced with actions and observations, the first corresponding to the operations and the second to the queries provided by the data structure. The abstraction level is high enough to capture intuitive and common assumptions as well as general and simple strategies used by programmers, and yet it contains sufficient structure to support the automated generation of concrete solutions (in the form of controllers). From such controllers and the use of standard data structures, an actual program in a general language like C++ or Python can be easily obtained. Then, we discuss how the resulting generalized planning problem can be reduced to an LTL synthesis problem, thus making available any LTL synthesis engine for obtaining the controllers. We illustrate the effectiveness of the approach on a series of examples.

TCS Journal 2020 Journal Article

Model-checking graded computation-tree logic with finite path semantics

• Aniello Murano
• Mimmo Parente
• Sasha Rubin
• Loredana Sorrentino

This paper introduces Graded Computation Tree Logic with finite path semantics (GCTL f ⁎, for short), a variant of Computation Tree Logic CTL⁎, in which path quantifiers are interpreted over finite paths and can count the number of such paths. State formulas of GCTL f ⁎ are interpreted over Kripke structures. The syntax of GCTL f ⁎ has path quantifiers of the form E ≥ g ψ which express that there are at least g many distinct finite paths that satisfy ψ. After defining and justifying the logic GCTL f ⁎, we solve its model checking problem and establish that its computational complexity is PSPACE-complete. Moreover, we investigate GCTL f ⁎ under the imperfect information setting. Precisely, we introduce GCTLK f ⁎, an epistemic extension of GCTL f ⁎ and prove that the model checking problem also in this case is PSPACE-complete.

GandALF Workshop 2020 Workshop Paper

Optimal Strategies in Weighted Limit Games

• Aniello Murano
• Sasha Rubin
• Martin Zimmermann

We prove the existence and computability of optimal strategies in weighted limit games, zero-sum infinite-duration games with a Büchi-style winning condition requiring to produce infinitely many play prefixes that satisfy a given regular specification. Quality of plays is measured in the maximal weight of infixes between successive play prefixes that satisfy the specification.

TCS Journal 2020 Journal Article

Preface

• Aniello Murano
• Sasha Rubin

IJCAI Conference 2020 Conference Paper

Pure-Past Linear Temporal and Dynamic Logic on Finite Traces

• Giuseppe De Giacomo
• Antonio Di Stasio
• Francesco Fuggitti
• Sasha Rubin

We review PLTLf and PLDLf, the pure-past versions of the well-known logics on finite traces LTLf and LDLf, respectively. PLTLf and PLDLf are logics about the past, and so scan the trace backwards from the end towards the beginning. Because of this, we can exploit a foundational result on reverse languages to get an exponential improvement, over LTLf /LDLf, for computing the corresponding DFA. This exponential improvement is reflected in several forms of sequential decision making involving temporal specifications, such as planning and decision problems in non-deterministic and non-Markovian domains. Interestingly, PLTLf (resp. , PLDLf ) has the same expressive power as LTLf (resp. , LDLf ), but transforming a PLTLf (resp. , PLDLf ) formula into its equivalent LTLf (resp. ,LDLf) is quite expensive. Hence, to take advantage of the exponential improvement, properties of interest must be directly expressed in PLTLf /PLDLf.

ICAPS Conference 2020 Conference Paper

Stochastic Fairness and Language-Theoretic Fairness in Planning in Nondeterministic Domains

• Benjamin Aminof
• Giuseppe De Giacomo
• Sasha Rubin

We address two central notions of fairness in the literature of nondeterministic fully observable domains. The first, which we call stochastic fairness, is classical, and assumes an environment which operates probabilistically using possibly unknown probabilities. The second, which is language-theoretic, assumes that if an action is taken from a given state infinitely often then all its possible outcomes should appear infinitely often; we call this state-action fairness. While the two notions coincide for standard reachability goals, they differ for temporally extended goals. This important difference has been overlooked in the planning literature and has led to the use of a product-based reduction in a number of published algorithms which were stated for state-action fairness, for which they are incorrect, while being correct for stochastic fairness. We remedy this and provide a correct optimal algorithm for solving state-action fair planning for ltl/ltlf goals, as well as a correct proof of the lower bound of the goal-complexity. Our proof is general enough that it also provides, for the no-fairness and stochastic-fairness cases, multiple missing lower bounds and new proofs of known lower bounds. Overall, we show that stochastic fairness is better behaved than state-action fairness.

IJCAI Conference 2020 Conference Paper

Synthesizing strategies under expected and exceptional environment behaviors

• Benjamin Aminof
• Giuseppe De Giacomo
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We consider an agent that operates with two models of the environment: one that captures expected behaviors and one that captures additional exceptional behaviors. We study the problem of synthesizing agent strategies that enforce a goal against environments operating as expected while also making a best effort against exceptional environment behaviors. We formalize these concepts in the context of linear-temporal logic, and give an algorithm for solving this problem. We also show that there is no trade-off between enforcing the goal under the expected environment specification and making a best-effort for it under the exceptional one.

AIJ Journal 2020 Journal Article

Verification of multi-agent systems with public actions against strategy logic

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

Model checking multi-agent systems, in which agents are distributed and thus may have different observations of the world, against strategic behaviours is known to be a complex problem in a number of settings. There are traditionally two ways of ameliorating this complexity: imposing a hierarchy on the observations of the agents, or restricting agent actions so that they are observable by all agents. We study systems of the latter kind, since they are more suitable for modelling rational agents. In particular, we define multi-agent systems in which all actions are public and study the model checking problem of such systems against Strategy Logic with equality, a very rich strategic logic that can express relevant concepts such as Nash equilibria, Pareto optimality, and due to the novel addition of equality, also evolutionary stable strategies. The main result is that the corresponding model checking problem is decidable.

ICAPS Conference 2019 Conference Paper

Planning under LTL Environment Specifications

• Benjamin Aminof
• Giuseppe De Giacomo
• Aniello Murano
• Sasha Rubin

Planning domains represent what an agent assumes or believes about the environment it acts in. In the presence of nondeterminism, additional temporal assumptions, such as fairness, are often expressed as extra conditions on the domain. Here we consider environment specifications expressed in arbitrary LTL, which generalize many forms of environment specifications, including classical specifications of nondeterministic domains, fairness, and other forms of linear-time constraints on the domain itself. Existing literature typically implicitly or explicitly considers environment specifications as constraints on possible traces. In contrast, in spite of the fact that we use a linear-time formalism, we propose to consider environment specifications as specifications of environment strategies. Planning in this framework is the problem of computing an agent strategy that achieves its goal against all environment strategies satisfying the specification. We study the mathematical and computational properties of planning in this general setting. We observe that not all LTL formulas correspond to legitimate environment specifications, and formally characterize the ones that do. Moreover, we show that our notion of planning generalizes the classical notion of Church’s synthesis, and that in spite this one can still solve it optimally using classical Church’s synthesis.

IJCAI Conference 2019 Conference Paper

Probabilistic Strategy Logic

• Benjamin Aminof
• Marta Kwiatkowska
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We introduce Probabilistic Strategy Logic, an extension of Strategy Logic for stochastic systems. The logic has probabilistic terms that allow it to express many standard solution concepts, such as Nash equilibria in randomised strategies, as well as constraints on probabilities, such as independence. We study the model-checking problem for agents with perfect- and imperfect-recall. The former is undecidable, while the latter is decidable in space exponential in the system and triple-exponential in the formula. We identify a natural fragment of the logic, in which every temporal operator is immediately preceded by a probabilistic operator, and show that it is decidable in space exponential in the system and the formula, and double-exponential in the nesting depth of the probabilistic terms. Taking a fixed nesting depth, this gives a fragment that still captures many standard solution concepts, and is decidable in exponential space.

AAMAS Conference 2019 Conference Paper

Reasoning about Changes of Observational Power in Logics of Knowledge and Time

• Aurèle Barrière
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study dynamic changes of agents’ observational power in logics of knowledge and time. We consider CTL∗K, the extension of CTL∗ with knowledge operators, and enrich it with a new operator that models a change in an agent’s way of observing the system. We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observational power, and we show that this new operator increases the expressivity of CTL∗K. We reduce the model-checking problem for our logic to that for CTL∗K, which is known to be decidable. This provides a solution to the model-checking problem for our logic, but it is not optimal, and we provide a direct model-checking procedure with better complexity.

IJCAI Conference 2018 Conference Paper

Alternating-time Temporal Logic on Finite Traces

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We develop a logic-based technique to analyse finite interactions in multi-agent systems. We introduce a semantics for Alternating-time Temporal Logic (for both perfect and imperfect recall) and its branching-time fragments in which paths are finite instead of infinite. We study validities of these logics and present optimal algorithms for their model-checking problems in the perfect recall case.

IJCAI Conference 2018 Conference Paper

Automata-Theoretic Foundations of FOND Planning for LTLf and LDLf Goals

• Giuseppe De Giacomo
• Sasha Rubin

We study planning for LTLf and LDLf temporally extended goals in nondeterministic fully observable domains (FOND). We consider both strong and strong cyclic plans, and develop foundational automata-based techniques to deal with both cases. Using these techniques we provide the computational characterization of both problems, separating the complexity in the size of the domain specification from that in the size of the formula. Specifically we establish them to be EXPTIME-complete and 2EXPTIME-complete, respectively, for both problems. In doing so, we also show 2EXPTIME-hardness for strong cyclic plans, which was open.

KR Conference 2018 Short Paper

Changing Observations in Epistemic Temporal Logic

• Aurèle Barrière
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

We study dynamic changes of agents’ observational power in logics of knowledge and time. We consider CTL∗ K, the extension of CTL∗ with knowledge operators, and enrich it with a new operator that models a change in an agent’s way of observing the system. We extend the classic semantics of knowledge for agents with perfect recall to account for changes of observation, and we show that this new operator strictly increases the expressivity of CTL∗ K. We also provide a modelchecking procedure for the logic we introduce, which has the same complexity as the best known model-checking procedure for the less expressive logic CTL∗ K.

I&C Journal 2018 Journal Article

CTL* with graded path modalities

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin

Graded path modalities count the number of paths satisfying a property, and generalize the existential ( E ) and universal ( A ) path modalities of Image 1. The resulting logic is denoted G Image 1, and is a powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We establish the complexity of the satisfiability problem of G Image 1, i. e. , 2ExpTime-Complete, the complexity of the model checking problem of G Image 1, i. e. , PSpace-Complete, and the complexity of the realizability/synthesis problem of G Image 1, i. e. , 2ExpTime-Complete. The lower bounds already hold for Image 1, and so we supply the upper bounds. The significance of this work is that G Image 1 is much more expressive than Image 1 as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.

AAMAS Conference 2018 Conference Paper

Decidable Verification of Multi-agent Systems with Bounded Private Actions

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

I&C Journal 2018 Journal Article

Graded modalities in Strategy Logic

• Benjamin Aminof
• Vadim Malvone
• Aniello Murano
• Sasha Rubin

Strategy Logic (SL) is a logical formalism for strategic reasoning in multi-agent systems. Its main feature is that it has variables for strategies that are associated to specific agents using a binding operator. In this paper we introduce Graded Strategy Logic (GradedSL), an extension of SL by graded quantifiers over tuples of strategy variables, i. e. , “there exist at least g different tuples ( x 1, .. ., x n ) of strategies” where g is a cardinal from the set N ∪ { ℵ 0, ℵ 1, 2 ℵ 0 }. We prove that the model-checking problem of GradedSL is decidable. We then turn to the complexity of fragments of GradedSL. When the g's are restricted to finite cardinals, written Graded N SL, the complexity of model-checking is no harder than for SL, i. e. , it is non-elementary in the quantifier-block rank. We illustrate our formalism by showing how to count the number of different strategy profiles that are Nash equilibria (NE). By analysing the structure of the specific formulas involved, we conclude that the important problem of checking for the existence of a unique NE can be solved in 2ExpTime, which is not harder than merely checking for the existence of such an equilibrium.

KR Conference 2018 Short Paper

Planning and Synthesis Under Assumptions

• Benjamin Aminof
• Giuseppe De Giacomo
• Aniello Murano
• Sasha Rubin

CSL Conference 2018 Conference Paper

Quantifying Bounds in Strategy Logic

• Nathanaël Fijalkow
• Bastien Maubert
• Aniello Murano
• Sasha Rubin

Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.

I&C Journal 2017 Journal Article

First-cycle games

• Benjamin Aminof
• Sasha Rubin

First-cycle games (FCG) are played on a finite graph by two players who push a token along the edges until a vertex is repeated, and a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of labels of the edges (or nodes) forming this cycle. These games are intimately connected with classic infinite-duration games such as parity and mean-payoff games. We initiate the study of FCGs in their own right, as well as formalise and investigate the connection between FCGs and certain infinite-duration games. We establish that (for efficiently computable Y) the problem of solving FCGs is Pspace-complete; we show that the memory required to win FCGs is, in general, Θ ( n )! (where n is the number of nodes in the graph); and we give a full characterisation of those properties Y for which all FCGs are memoryless determined. We formalise the connection between FCGs and certain infinite-duration games and prove that strategies transfer between them. Using the machinery of FCGs, we provide a recipe that can be used to very easily deduce that many infinite-duration games, e. g. , mean-payoff, parity, and energy games, are memoryless determined.

IJCAI Conference 2017 Conference Paper

Generalized Planning: Non-Deterministic Abstractions and Trajectory Constraints

• Blai Bonet
• Giuseppe De Giacomo
• Hector Geffner
• Sasha Rubin

We study the characterization and computation of general policies for families of problems that share a structure characterized by a common reduction into a single abstract problem. Policies mu that solve the abstract problem P have been shown to solve all problems Q that reduce to P provided that mu terminates in Q. In this work, we shed light on why this termination condition is needed and how it can be removed. The key observation is that the abstract problem P captures the common structure among the concrete problems Q that is local (Markovian) but misses common structure that is global. We show how such global structure can be captured by means of trajectory constraints that in many cases can be expressed as LTL formulas, thus reducing generalized planning to LTL synthesis. Moreover, for a broad class of problems that involve integer variables that can be increased or decreased, trajectory constraints can be compiled away, reducing generalized planning to fully observable non-deterministic planning.

IJCAI Conference 2017 Conference Paper

Nash Equilibria in Concurrent Games with Lexicographic Preferences

• Julian Gutierrez
• Aniello Murano
• Giuseppe Perelli
• Sasha Rubin
• Michael Wooldridge

We study concurrent games with finite-memory strategies where players are given a Buchi and a mean-payoff objective, which are related by a lexicographic order: a player first prefers to satisfy its Buchi objective, and then prefers to minimise costs, which are given by a mean-payoff function. In particular, we show that deciding the existence of a strict Nash equilibrium in such games is decidable, even if players' deviations are implemented as infinite memory strategies.

IJCAI Conference 2017 Conference Paper

Verification of Broadcasting Multi-Agent Systems against an Epistemic Strategy Logic

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

We study a class of synchronous, perfect-recall multi-agent systemswith imperfect information and broadcasting (i. e. , fully observableactions). We define an epistemic extension of strategy logic withincomplete information and the assumption of uniform and coherentstrategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is decidable with non-elementarycomplexity. We exemplify the applicability of the framework on arational secret-sharing scenario.

AAMAS Conference 2017 Conference Paper

Verification of Multi-agent Systems with Imperfect Information and Public Actions

• Francesco Belardinelli
• Alessio Lomuscio
• Aniello Murano
• Sasha Rubin

AAMAS Conference 2016 Conference Paper

Automatic Verification of Multi-Agent Systems in Parameterised Grid-Environments

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin
• Florian Zuleger

We present a framework for modeling and analysing multiple mobile agents on grid-environments such as finite mazes and labyrinths. Agents are modeled as automata, and the grid-environments are parameterised by their size and the relative positions of the obstacles. We study the verification problem, i. e. , whether given agents complete a given task on a given (possibly infinite) set of grid-environments. We identify restrictions on the agents and on the environments for which the verification problem is decidable (and in pspace). These assumptions are: i) there are a bounded number of obstacles, and ii) the agents are not allowed to issue commands like “increase my x-coordinate by 1” but can only issue commands that change their relative positions, e. g. , “increase my x-coordinate until I go past this wall”. We prove pspace-hardness already for the verification problem of a single agent on singleton parameterised environments with no obstacles. It is therefore remarkable that the pspace-upper bound also holds for the verification problem with multiple agents, parameterised environments and multiple obstacles. We prove that weakening either of restrictions i) or ii) results in undecidability. The importance of this work is that it is the first to give a sound and complete decision procedure for the verification problem on parameterised grid-like environments. Previous work either involved only a single grid, restricted the scheduling of the agents, or excluded grids altogether. General Terms Theory, Verification

AAMAS Conference 2016 Conference Paper

Graded Strategy Logic: Reasoning about Uniqueness of Nash Equilibria

• Benjamin Aminof
• Vadim Malvone
• Aniello Murano
• Sasha Rubin

Strategy Logic (SL) is a well established formalism for strategic reasoning in multi-agent systems. In a nutshell, SL is built over LTL and treats strategies as first-order objects that can be associated with agents by means of a binding operator. In this work we introduce Graded Strategy Logic (Graded- SL), an extension of SL by graded quantifiers over tuples of strategy variables such as “there exist at least g different tuples (x1, .. ., xn) of strategies”. We study the model-checking problem of Graded-SL and prove that it is no harder than for SL, i. e. , it is non-elementary in the quantifier rank. We show that Graded-SL allows one to count the number of different strategy profiles that are Nash equilibria (NE), or subgame-perfect equilibria (SPE). By analyzing the structure of the specific formulas involved, we conclude that the important problems of checking for the existence of a unique NE or SPE can both be solved in 2ExpTime, which is not harder than merely checking for the existence of such equilibria.

IJCAI Conference 2016 Conference Paper

Imperfect-Information Games and Generalized Planning

• Giuseppe De Giacomo
• Aniello Murano
• Sasha Rubin
• Antonio Di Stasio

We study a generalized form of planning under partial observability, in which we have multiple, possibly infinitely many, planning domains with the same actions and observations, and goals expressed over observations, which are possibly temporally extended. By building on work on two-player (non-probabilistic) games with imperfect information in the Formal Methods literature, we devise a general technique, generalizing the belief-state construction, to remove partial observability. This reduces the planning problem to a game of perfect information with a tight correspondence between plans and strategies. Then we instantiate the technique and solve some generalized-planning problems.

KR Conference 2016 Conference Paper

Prompt Alternating-Time Epistemic Logics

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin
• Florian Zuleger

In temporal logics, the operator F expresses that at some time in the future something happens, e. g., a request is eventually granted. Unfortunately, there is no bound on the time until the eventuality is satisfied which in many cases does not correspond to the intuitive meaning system designers have, namely, that F abstracts the idea that there is a bound on this time although its magnitude is not known. An elegant way to capture this meaning is through Prompt-LTL, which extends LTL with the operator FP (“prompt eventually”). We extend this work by studying alternating-time epistemic temporal logics extended with FP. We study the model-checking problem of the logic PromptKATL∗, which is ATL∗ extended with epistemic operators and prompt eventually. We also obtain results for the modelchecking problem of some of its fragments. Namely, of Prompt-KATL (ATL with epistemic operators and prompt eventually), Prompt-KCTL∗ (CTL∗ with epistemic operators and prompt eventually), and finally the existential fragments of Prompt-KATL∗ and Prompt-KATL.

LPAR Conference 2015 Conference Paper

On CTL* with Graded Path Modalities

• Benjamin Aminof
• Aniello Murano
• Sasha Rubin

Abstract Graded path modalities count the number of paths satisfying a property, and generalize the existential ( \(\mathsf {E}\) ) and universal \((\mathsf {A})\) path modalities of \(\textsc {CTL}^{*}\). The resulting logic is denoted \(\textsc {G}\textsc {CTL}^{*}\), and is a very powerful logic since (as we show) it is equivalent, over trees, to monadic path logic. We settle the complexity of the satisfiability problem of \(\textsc {G}\textsc {CTL}^{*}\), i. e. , 2 ExpTime - Complete, and the complexity of the model checking problem of \(\textsc {G}\textsc {CTL}^{*}\), i. e. , PSpace - Complete. The lower bounds already hold for \(\textsc {CTL}^{*}\), and so we supply the upper bounds. The significance of this work is two-fold: \(\textsc {G}\textsc {CTL}^{*}\) is much more expressive than \(\textsc {CTL}^{*}\) as it adds to it a form of quantitative reasoning, and this is done at no extra cost in computational complexity.

LPAR Conference 2015 Conference Paper

On the Expressive Power of Communication Primitives in Parameterised Systems

• Benjamin Aminof
• Sasha Rubin
• Florian Zuleger

Abstract We study foundational problems regarding the expressive power of parameterised systems. These (infinite-state) systems are composed of arbitrarily many finite-state processes that synchronise using a given communication primitive, i. e. , broadcast, asynchronous rendezvous, broadcast with message loss, pairwise rendezvous, or disjunctive guards. With each communication primitive we associate the class of parameterised systems that use it. We study the relative expressive power of these classes (can systems in one class be simulated by systems in another?) and provide a complete picture with only a single question left open. Motivated by the question of separating these classes, we also study the absolute expressive power (e. g. , is the set of traces of every parameterised system of a given class \(\omega \) -regular?). Our work gives insight into the verification and synthesis of parameterised systems, including new decidability and undecidability results for model checking parameterised systems using broadcast with message loss and asynchronous rendezvous.

Highlights Conference 2015 Conference Abstract

Parameterised Verification: Recent Advances

• Sasha Rubin

TCS Journal 2014 Journal Article

Alternating traps in Muller and parity games

• Andrey Grinshpun
• Pakawat Phalitnonkiat
• Sasha Rubin
• Andrei Tarfulea

Muller games are played by two players moving a token along a graph; the winner is determined by the set of vertices that occur infinitely often. The central algorithmic problem is to compute the winning regions for the players. Different classes and representations of Muller games lead to problems of varying computational complexity. One such class are parity games; these are of particular significance in computational complexity, as they remain one of the few combinatorial problems known to be in NP ∩ co-NP but not known to be in P. We show that winning regions for a Muller game can be determined from the alternating structure of its traps. To every Muller game we then associate a natural number that we call its trap depth; this parameter measures how complicated the trap structure is. We present algorithms for parity games that run in polynomial time for graphs of bounded trap depth, and in general run in time exponential in the trap depth.

Highlights Conference 2014 Conference Abstract

First Cycle Games

• Sasha Rubin

First cycle games (FCGs) are played on a finite graph by two players who push a token along the edges of the graph until a simple cycle is formed. The winner is determined by some fixed property Y of the sequence of nodes forming this cycle. We are motivated by two questions: Under what conditions on Y is every FCG memoryless determined? What is the connection between FCGs and traditional winning conditions such as mean-payoff games? Our answers to these questions take the following form: we generalise the proof by Ehrenfeucht and Mycielski that mean-payoff games are memoryless determined and then supply a recipe for proving that a winning condition is memoryless determined. All memoryless determined infinite duration games that we are aware of can be proved memoryless determined using this recipe.

GandALF Workshop 2012 Workshop Paper

A Myhill-Nerode theorem for automata with advice

• Alex Kruckman
• Sasha Rubin
• John Sheridan
• Ben Zax

An automaton with advice is a finite state automaton which has access to an additional fixed infinite string called an advice tape. We refine the Myhill-Nerode theorem to characterize the languages of finite strings that are accepted by automata with advice. We do the same for tree automata with advice.

CSL Conference 2005 Conference Paper

Decidability of Term Algebras Extending Partial Algebras

• Bakhadyr Khoussainov
• Sasha Rubin

Abstract Let \({\cal A}\) be a partial algebra on a finite signature. We say that \({\cal A}\) has decidable query evaluation problem if there exists an algorithm that given a first order formula \(\phi(\bar{x})\) and a tuple \(\bar{a}\) from the domain of \({\cal A}\) decides whether or not \(\phi(\bar{a})\) holds in \({\cal A}\). Denote by \(E({\cal A})\) the total algebra freely generated by \({\cal A}\). We prove that if \({\cal A}\) has a decidable query evaluation problem then so does \(E({\cal A})\). In particular, the first order theory of \(E({\cal A})\) is decidable. In addition, if \({\cal A}\) has elimination of quantifiers then so does \(E({\cal A})\) extended by finitely many definable selector functions and tester predicates. Our proof is a refinement of the quantifier elimination procedure for free term algebras. As an application we show that any finitely presented term algebra has a decidable query evaluation problem. This extends the known result that the word problem for finitely presented term algebras is decidable.