Search

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

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.

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., Comment: Changed formatting