arXiv subjects

Luca Di Stefano

Publications and source records attributed to Luca Di Stefano.

6 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↗

arXiv2025

Symbolic ω-automata with obligations

Extensions of ω-automata to infinite alphabets typically rely on symbolic guards to keep the transition relation finite, and on registers or memory cells to preserve information from past symbols. Symbolic transitions alone are ill-suited to act on this information, and register automata have intricate formal semantics and issues with tractability. We propose a slightly different approach based on obligations, i.e., assignment-like constructs attached to transitions. Whenever a transition with an obligation is taken, the obligation is evaluated against the current symbol and yields a constraint on the next symbol that the automaton will read. We formalize obligation automata with existential and universal branching and Emerson-Lei acceptance conditions, which subsume classic families such as Büchi, Rabin, Strett, and parity automata. We show that these automata recognise a strict superset of ω-regular languages. To illustrate the practicality of our proposal, we also introduce a machine-readable format to express obligation automata and describe a tool implementing several operations over them, including automata product and emptiness checking.

cs.FL↗

arXiv2025

Execution and monitoring of HOA automata with HOAX

We present a tool called Hoax for the execution of ω-automata expressed in the popular HOA format. The tool leverages the notion of trap sets to enable runtime monitoring of any (non-parity) acceptance condition supported by the format. When the automaton is not monitorable, the tool may still be able to recognise so-called ugly prefixes, and determine that no further observation will ever lead to a conclusive verdict. The tool is open-source and highly configurable. We present its formal foundations, its design, and compare it against the trace analyser PyContract on a lock acquisition scenario.

cs.LO↗

arXiv2025

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üchi 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↗

arXiv2021

Post-Metering Value-Added Services for Low Voltage Electricity Users: Lessons Learned From the Italian Experience of CHAIN 2

Electrical energy consumption data accessibility for low voltage end users is one of the pillars of smart grids. In some countries, despite the presence of smart meters, a fragmentary data availability and/or the lack of standardization hinders the creation of post-metering value-added services and confines such innovative solutions to the prototypal and experimental level. We take inspiration from the technology adopted in Italy, where the national regulatory authority actively supported the definition of a solution agreed upon by all the involved stakeholders. In this context, smart meters are enabled to convey data to low voltage end users through a power line communication channel (CHAIN 2) in near real-time. The aim of this paper is twofold. On the one hand, it describes the proof of concept that the channel underwent and its subsequent validation (with performances nearing 99% success rate). On the other hand, it defines a classification framework (I2MA) for post-metering value-added services, in order to categorize each use case based on both level of service and expected benefits, and understand its maturity level. As an example, we apply the methodology to the 16 use cases defined in Italy. The lessons learned from the regulatory, technological, and functional approach of the Italian experience bring us to the provision of recommendations for researchers and industry experts. In particular, we argue that a well-functioning post-metering value-added services' market can flourish when: i) distribution system operators certify the measurements coming from smart meters; ii) national regulatory authorities support the technological innovation needed for setting up this market; and iii) service providers create customer-oriented solutions based on smart meters' data.

eess.SY↗

arXiv2018

Towards formal models and languages for verifiable Multi-Robot Systems

Incorrect operations of a Multi-Robot System (MRS) may not only lead to unsatisfactory results, but can also cause economic losses and threats to safety. These threats may not always be apparent, since they may arise as unforeseen consequences of the interactions between elements of the system. This call for tools and techniques that can help in providing guarantees about MRSs behaviour. We think that, whenever possible, these guarantees should be backed up by formal proofs to complement traditional approaches based on testing and simulation. We believe that tailored linguistic support to specify MRSs is a major step towards this goal. In particular, reducing the gap between typical features of an MRS and the level of abstraction of the linguistic primitives would simplify both the specification of these systems and the verification of their properties. In this work, we review different agent-oriented languages and their features; we then consider a selection of case studies of interest and implement them useing the surveyed languages. We also evaluate and compare effectiveness of the proposed solution, considering, in particular, easiness of expressing non-trivial behaviour.

cs.PL↗