arXiv subjects

Rayna Dimitrova

Publications and source records attributed to Rayna Dimitrova.

At least 19 recordsLinked to original sources

arXiv2026

Modular Attractor Acceleration in Infinite-State Games (Full Version)

Infinite-state games provide a framework for the synthesis of reactive systems with unbounded data domains. Solving such games typically relies on computing symbolic fixpoints, particularly symbolic attractors. However, these computations may not terminate, and while recent acceleration techniques have been proposed to address this issue, they often rely on acceleration arguments of limited expressiveness. In this work, we propose an approach for the modular computation of acceleration arguments. It enables the construction of complex acceleration arguments by composing simpler ones, thereby improving both scalability and flexibility. In addition, we introduce a summarization technique that generalizes discovered acceleration arguments, allowing them to be efficiently reused across multiple contexts. Together, these contributions improve the efficiency of solving infinite-state games in reactive synthesis, as demonstrated by our experimental evaluation.

cs.LO↗

arXiv2025

Synthesis of Communication Policies for Multi-Agent Systems Robust to Communication Restrictions

We study stochastic multi-agent systems in which agents must cooperate to maximize the probability of achieving a common reach-avoid objective. In many applications, during the execution of the system, the communication between the agents can be constrained by restrictions on the bandwidth currently available for exchanging local-state information between the agents. In this paper, we propose a method for computing joint action and communication policies for the group of agents that aim to satisfy the communication restrictions as much as possible while achieving the optimal reach-avoid probability when communication is unconstrained. Our method synthesizes a pair of action and communication policies robust to restrictions on the number of agents allowed to communicate. To this end, we introduce a novel cost function that measures the amount of information exchanged beyond what the communication policy allows. We evaluate our approach experimentally on a range of benchmarks and demonstrate that it is capable of computing pairs of action and communication policies that satisfy the communication restrictions, if such exist.

cs.MA↗

arXiv2025

Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems

The synthesis of infinite-state reactive systems from temporal logic specifications or infinite-state games has attracted significant attention in recent years, leading to the emergence of novel solving techniques. Most approaches are accompanied by an implementation showcasing their viability on an increasingly larger collection of benchmarks. Those implementations are -- often simple -- prototypes. Furthermore, differences in specification formalisms and formats make comparisons difficult, and writing specifications is a tedious and error-prone task. To address this, we present Issy, a tool for specification, realizability, and synthesis of infinite-state reactive systems. Issy comes with an expressive specification language that allows for combining infinite-state games and temporal formulas, thus encompassing the current formalisms. The realizability checking and synthesis methods implemented in Issy build upon recently developed approaches and extend them with newly engineered efficient techniques, offering a portfolio of solving algorithms. We evaluate Issy on an extensive set of benchmarks, demonstrating its competitiveness with the state of the art. Furthermore, Issy provides tooling for a general high-level format designed to make specification easier for users. It also includes a compiler to a more machine-readable format that other tool developers can easily use, which we hope will lead to a broader adoption and advances in infinite-state reactive synthesis.

cs.LO↗

arXiv2024

Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements

Quantitative requirements play an important role in the context of multi-agent systems, where there is often a trade-off between the tasks of individual agents and the constraints that the agents must jointly adhere to. We study multi-agent systems whose requirements are formally specified in the quantitative temporal logic LTL[$\mathcal{F}$] as a combination of local task specifications for the individual agents and a shared safety constraint, The intricate dependencies between the individual agents entailed by their local and shared objectives make the design of multi-agent systems error-prone, and their verification time-consuming. In this paper we address this problem by proposing a novel notion of quantitative assume-guarantee contracts, that enables the compositional design and verification of multi-agent systems with quantitative temporal specifications. The crux of these contracts lies in their ability to capture the coordination between the individual agents to achieve an optimal value of the overall specification under any possible behavior of the external environment. We show that the proposed framework improves the scalability and modularity of formal verification of multi-agent systems against quantitative temporal specifications.

cs.LO↗

arXiv2024

Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis (Full Version)

Infinite-state reactive synthesis has attracted significant attention in recent years, which has led to the emergence of novel symbolic techniques for solving infinite-state games. Temporal logics featuring variables over infinite domains offer an expressive high-level specification language for infinite-state reactive systems. Currently, the only way to translate these temporal logics into symbolic games is by naively encoding the specification to use techniques designed for the Boolean case. An inherent limitation of this approach is that it results in games in which the semantic structure of the temporal and first-order constraints present in the formula is lost. There is a clear need for techniques that leverage this information in the translation process to speed up solving the generated games. In this work, we propose the first approach that addresses this gap. Our technique constructs a monitor incorporating first-order and temporal reasoning at the formula level, enriching the constructed game with semantic information that leads to more efficient solving. We demonstrate that thanks to this, our method outperforms the state-of-the-art techniques across a range of benchmarks.

cs.LO↗

arXiv2024

Localized Attractor Computations for Infinite-State Games (Full Version)

Infinite-state games are a commonly used model for the synthesis of reactive systems with unbounded data domains. Symbolic methods for solving such games need to be able to construct intricate arguments to establish the existence of winning strategies. Often, large problem instances require prohibitively complex arguments. Therefore, techniques that identify smaller and simpler sub-problems and exploit the respective results for the given game-solving task are highly desirable. In this paper, we propose the first such technique for infinite-state games. The main idea is to enhance symbolic game-solving with the results of localized attractor computations performed in sub-games. The crux of our approach lies in identifying useful sub-games by computing permissive winning strategy templates in finite abstractions of the infinite-state game. The experimental evaluation of our method demonstrates that it outperforms existing techniques and is applicable to infinite-state games beyond the state of the art.

cs.LO↗

arXiv2023

Solving Infinite-State Games via Acceleration (Full Version)

Two-player graph games have found numerous applications, most notably in the synthesis of reactive systems from temporal specifications, but also in verification. The relevance of infinite-state systems in these areas has lead to significant attention towards developing techniques for solving infinite-state games. We propose novel symbolic semi-algorithms for solving infinite-state games with temporal winning conditions. The novelty of our approach lies in the introduction of an acceleration technique that enhances fixpoint-based game-solving methods and helps to avoid divergence. Classical fixpoint-based algorithms, when applied to infinite-state games, are bound to diverge in many cases, since they iteratively compute the set of states from which one player has a winning strategy. Our proposed approach can lead to convergence in cases where existing algorithms require an infinite number of iterations. This is achieved by acceleration: computing an infinite set of states from which a simpler sub-strategy can be iterated an unbounded number of times in order to win the game. Ours is the first method for solving infinite-state games to employ acceleration. Thanks to this, it is able to outperform state-of-the-art techniques on a range of benchmarks, as evidenced by our evaluation of a prototype implementation.

cs.LO↗

arXiv2023

Taming Large Bounds in Synthesis from Bounded-Liveness Specifications (Full Version)

Automatic synthesis from temporal logic specifications is an attractive alternative to manual system design, due to its ability to generate correct-by-construction implementations from high-level specifications. Due to the high complexity of the synthesis problem, significant research efforts have been directed at developing practically efficient approaches for restricted specification language fragments. In this paper, we focus on the Safety LTL fragment of Linear Temporal Logic (LTL) syntactically extended with bounded temporal operators. We propose a new synthesis approach with the primary motivation to solve efficiently the synthesis problem for specifications with bounded temporal operators, in particular those with large bounds. The experimental evaluation of our method shows that for this type of specifications, it outperforms state-of-art synthesis tools, demonstrating that it is a promising approach to efficiently treating quantitative timing constraints in safety specifications.

cs.LO↗

arXiv2020

Synthesizing Approximate Implementations for Unrealizable Specifications

The unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this paper, we present algorithms for synthesis in bounded environments, where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative implementations from unrealizable specifications. Such implementations may violate the specification in general, but are guaranteed to satisfy the specification on at least a specified portion of the bounded-size lassos. We evaluate the algorithms on different arbiter specifications.

cs.LO↗

arXiv2020

Approximate Automata for Omega-Regular Languages

Automata over infinite words, also known as omega-automata, play a key role in the verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two characteristics: the acceptance condition (e.g. B\"uchi or parity) and the determinism (e.g., deterministic or nondeterministic) of an automaton. These characteristics play a crucial role in applications of automata theory. For example, certain acceptance conditions can be handled more efficiently than others by dedicated tools and algorithms. Furthermore, some applications, such as synthesis and probabilistic model checking, require that properties are represented as some type of deterministic omega-automata. However, properties cannot always be represented by automata with the desired acceptance condition and determinism. In this paper we study the problem of approximating linear-time properties by automata in a given class. Our approximation is based on preserving the language up to a user-defined precision given in terms of the size of the finite lasso representation of infinite executions that are preserved. We study the state complexity of different types of approximating automata, and provide constructions for the approximation within different automata classes, for example, for approximating a given automaton by one with a simpler acceptance condition.

cs.FL↗

arXiv2020

Conformance Relations and Hyperproperties for Doping Detection in Time and Space

We present a novel and generalised notion of doping cleanness for cyber-physical systems that allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing notions of conformance for cyber-physical systems. As a formal basis for monitoring conformance-based cleanness, we develop the temporal logic HyperSTL*, an extension of Signal Temporal Logics with trace quantifiers and a freeze operator. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests.

cs.LO↗

arXiv2020

Near-Optimal Reactive Synthesis Incorporating Runtime Information

We consider the problem of optimal reactive synthesis - compute a strategy that satisfies a mission specification in a dynamic environment, and optimizes a performance metric. We incorporate task-critical information, that is only available at runtime, into the strategy synthesis in order to improve performance. Existing approaches to utilising such time-varying information require online re-synthesis, which is not computationally feasible in real-time applications. In this paper, we pre-synthesize a set of strategies corresponding to candidate instantiations (pre-specified representative information scenarios). We then propose a novel switching mechanism to dynamically switch between the strategies at runtime while guaranteeing all safety and liveness goals are met. We also characterize bounds on the performance suboptimality. We demonstrate our approach on two examples - robotic motion planning where the likelihood of the position of the robot's goal is updated in real-time, and an air traffic management problem for urban air mobility.

cs.RO↗

arXiv2020

Probabilistic Hyperproperties of Markov Decision Processes

Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.

cs.LO↗

arXiv2019

Reactive Synthesis with Maximum Realizability of Linear Temporal Logic Specifications

A challenging problem for autonomous systems is to synthesize a reactive controller that conforms to a set of given correctness properties. Linear temporal logic (LTL) provides a formal language to specify the desired behavioral properties of systems. In applications in which the specifications originate from various aspects of the system design, or consist of a large set of formulas, the overall system specification may be unrealizable. Driven by this fact, we develop an optimization variant of synthesis from LTL formulas, where the goal is to design a controller that satisfies a set of hard specifications and minimally violates a set of soft specifications. To that end, we introduce a value function that, by exploiting the LTL semantics, quantifies the level of violation of properties. Inspired by the idea of bounded synthesis, we fix a bound on the implementation size and search for an implementation that is optimal with respect to the said value function. We propose a novel maximum satisfiability encoding of the search for an optimal implementation (within the given bound on the implementation size). We iteratively increase the bound on the implementation size until a termination criterion, such as a threshold over the value function, is met.

cs.FL↗

arXiv2019

Distributed Synthesis of Surveillance Strategies for Mobile Sensors

We study the problem of synthesizing strategies for a mobile sensor network to conduct surveillance in partnership with static alarm triggers. We formulate the problem as a multi-agent reactive synthesis problem with surveillance objectives specified as temporal logic formulas. In order to avoid the state space blow-up arising from a centralized strategy computation, we propose a method to decentralize the surveillance strategy synthesis by decomposing the multi-agent game into subgames that can be solved independently. We also decompose the global surveillance specification into local specifications for each sensor, and show that if the sensors satisfy their local surveillance specifications, then the sensor network as a whole will satisfy the global surveillance objective. Thus, our method is able to guarantee global surveillance properties in a mobile sensor network while synthesizing completely decentralized strategies with no need for coordination between the sensors. We also present a case study in which we demonstrate an application of decentralized surveillance strategy synthesis.

cs.AI↗

arXiv2019

Causality Analysis for Concurrent Reactive Systems (Extended Abstract)

We present a comprehensive language theoretic causality analysis framework for explaining safety property violations in the setting of concurrent reactive systems. Our framework allows us to uniformly express a number of causality notions studied in the areas of artificial intelligence and formal methods, as well as define new ones that are of potential interest in these areas. Furthermore, our formalization provides means for reasoning about the relationships between individual notions which have mostly been considered independently in prior work; and allows us to judge the appropriateness of the different definitions for various applications in system design. In particular, we consider causality analysis notions for debugging, error resilience, and liability resolution in concurrent reactive systems. Finally, we present automata-based algorithms for computing various causal sets based on our language-theoretic encoding, and derive the algorithmic complexities.

cs.FL↗

arXiv2018

Maximum Realizability for Linear Temporal Logic Specifications

Automatic synthesis from linear temporal logic (LTL) specifications is widely used in robotic motion planning, control of autonomous systems, and load distribution in power networks. A common specification pattern in such applications consists of an LTL formula describing the requirements on the behaviour of the system, together with a set of additional desirable properties. We study the synthesis problem in settings where the overall specification is unrealizable, more precisely, when some of the desirable properties have to be (temporarily) violated in order to satisfy the system's objective. We provide a quantitative semantics of sets of safety specifications, and use it to formalize the "best-effort" satisfaction of such soft specifications while satisfying the hard LTL specification. We propose an algorithm for synthesizing implementations that are optimal with respect to this quantitative semantics. Our method builds upon the idea of the bounded synthesis approach, and we develop a MaxSAT encoding which allows for maximizing the quantitative satisfaction of the safety specifications. We evaluate our algorithm on scenarios from robotics and power distribution networks.

cs.LO↗

arXiv2017

Synthesis of surveillance strategies via belief abstraction

We study the problem of synthesizing a controller for a robot with a surveillance objective, that is, the robot is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate this problem as a one-sided partial-information game in which the winning condition for the agent is specified as a temporal logic formula. The specification formalizes the surveillance requirement given by the user, including additional non-surveillance tasks. In order to synthesize a surveillance strategy that meets the specification, we transform the partial-information game into a perfect-information one, using abstraction to mitigate the exponential blow-up typically incurred by such transformations. This enables the use of off-the-shelf tools for reactive synthesis. We use counterexample-guided refinement to automatically achieve abstraction precision that is sufficient to synthesize a surveillance strategy. We evaluate the proposed method on two case-studies, demonstrating its applicability to large state-spaces and diverse requirements.

cs.RO↗