arXiv subjects

Shaun Azzopardi

Publications and source records attributed to Shaun Azzopardi.

8 recordsLinked to original sources

arXiv2026

sweap: Reactive Synthesis for Infinite-State Integer Problems

Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present sweap, a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. sweap implements a CEGAR approach, relying on state-of-the-art finite-state synthesis tools as black boxes to solve abstract synthesis problems. sweap supports most common input formalisms for infinite-state reactive-synthesis problems: Temporal Stream Logic Modulo Theories, Reactive Program Games, the bespoke input of the ISSY tool, and our own bespoke input. We present a mature version of sweap with novel features: a dual abstraction approach that improves its capabilities in proving unrealisability, support for nondeterministic and unbounded updates, more general initialization of variables, and equirealisable reductions for optimisation. Experimental evaluation shows that sweap outperforms its only competitor in this domain.

cs.LO↗

arXiv2024

Sound Conflict Analysis for Timed Contract Automata

One can find various temporal deontic logics in literature, most focusing on discrete time. The literature on real-time constraints and deontic norms is much sparser. Thus, many analysis techniques which have been developed for deontic logics have not been considered for continuous time. In this paper we focus on the notion of conflict analysis which has been extensively studied for discrete time deontic logics. We present a sound, but not complete algorithm for detecting conflicts in timed contract automata and prove the correctness of the algorithm, illustrating the analysis on a case study.

cs.LO↗

arXiv2024

A Direct Translation from LTL with Past to Deterministic Rabin Automata

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.

cs.FL↗

arXiv2023

Synchronous Agents, Verification, and Blame -- A Deontic View

A question we can ask of multi-agent systems is whether the agents' collective interaction satisfies particular goals or specifications, which can be either individual or collective. When a collaborative goal is not reached, or a specification is violated, a pertinent question is whether any agent is to blame. This paper considers a two-agent synchronous setting and a formal language to specify when agents' collaboration is required. We take a deontic approach and use obligations, permissions, and prohibitions to capture notions of non-interference between agents. We also handle reparations, allowing violations to be corrected or compensated. We give trace semantics to our logic, and use it to define blame assignment for violations. We give an automaton construction for the logic, which we use as the base for model checking and blame analysis. We also further provide quantitative semantics that is able to compare different interactions in terms of the required reparations.

cs.LO↗

arXiv2023

Full LTL Synthesis over Infinite-state Arenas

Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of steps is unbounded. Existing approaches struggle with this problem, or can handle at most deterministic games with B\"uchi goals. This work goes beyond by contributing the first effectual approach to synthesis with full LTL objectives, based on Boolean abstractions that encode both safety and liveness properties of the underlying infinite arena. We take a CEGAR approach: attempting synthesis on the Boolean abstraction, checking spuriousness of abstract counterstrategies through invariant checking, and refining the abstraction based on counterexamples. We reduce the complexity, when restricted to predicates, of abstracting and synthesising by an exponential through an efficient binary encoding. This also allows us to eagerly identify useful fairness properties. Our discrete synthesis tool outperforms the state-of-the-art on linear integer arithmetic (LIA) benchmarks from literature, solving almost double as many syntesis problems as the current state-of-the-art. It also solves slightly more problems than the second-best realisability checker, in one-third of the time. We also introduce benchmarks with richer objectives that other approaches cannot handle, and evaluate our tool on them.

cs.LO↗

arXiv2022

R-CHECK: A Model Checker for Verifying Reconfigurable MAS

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.

cs.LO↗

arXiv2021

Incorporating Monitors in Reactive Synthesis without Paying the Price

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.

cs.LO↗

arXiv2017

Control-Flow Residual Analysis for Symbolic Automata

Where full static analysis of systems fails to scale up due to system size, dynamic monitoring has been increasingly used to ensure system correctness. The downside is, however, runtime overheads which are induced by the additional monitoring code instrumented. To address this issue, various approaches have been proposed in the literature to use static analysis in order to reduce monitoring overhead. In this paper we generalise existing work which uses control-flow static analysis to optimise properties specified as automata, and prove how similar analysis can be applied to more expressive symbolic automata - enabling reduction of monitoring instrumentation in the system, and also monitoring logic. We also present empirical evidence of the effectiveness of this approach through an analysis of the effect of monitoring overheads in a financial transaction system.

cs.LO↗