Workshop on Synthesis, Monitoring and Learning (SMiLe)

Programme

Thursday, August 31
14:30 – 16:00	Luca Geatti Reactive Synthesis of the Safety Fragment of LTL – Efficient and Symbolic Algorithms
16:00 – 16:30	Coffee break
16:30 – 18:00	Leonardo Mangeruca Reactive Synthesis in the Aerospace Industry
Friday, September 1
09:30 – 11:00	Adrian Francalanza Extended Monitorability through Multiple Executions
11:00 – 11:30	Coffee break
11:30 – 13:00	Bernhard Aichernig Automata Learning and Testing in AALpy
13:00 – 14:00	Lunch

Talks

Luca Geatti

Reactive Synthesis of the Safety Fragment of LTL – Efficient and Symbolic Algorithms

In this talk, we focus on the reactive synthesis problem for the safety fragment of Linear Temporal Logic (LTL). Languages in this fragment express the fact that “something bad never happens” and are such that a prefix of a sequence suffices to establish whether it belongs or not to the language, allowing one to reason on finite sequences.

We first show classic algorithms for solving reactive synthesis of the safety fragment of LTL. Second, we focus on the importance of past temporal operators in lowering the complexity of problem. Third, we describe symbolic and efficient algorithms for reactive synthesis of some safety fragments of LTL.

Finally, we present a new safety fragment of Linear Temporal Logic with Past, called Extended Bounded Response LTL with Past (LTLEBR+P), which allows one to combine bounded and universal unbounded temporal operators and which is able to express all and only the safety properties definable in LTL. We show a symbolic algorithm for its reactive syntesis problem and we evaluate it on various benchmarks showing better performance with respect to other approaches for general LTL or safety fragments.

---

Leonardo Mangeruca

Reactive Synthesis in the Aerospace Industry

The complexity of modern aircraft development is rising constantly pushed by the growth of the transportation market, the continuous technology improvements, the rising of new technologies, the development of more challenging regulations, and the ever increasing competition. The high investment costs involved in the development of an aircraft and its constituent systems lead airframers and tier-1 suppliers to take critical design decisions early, with a potentially high risk on the development and operational costs of the aircraft. On the other hand, the increasing complexity makes the costs and risks connected with the verification and testing of aircraft systems and their integration constantly rising. The increasing electrification of the aircraft is responsible for a constant growth of the airborne software, introducing new opportunities for the optimized control of aircraft systems operations, but also leading to exponentially increasing costs of software verification.
These considerations are pushing the aerospace industry towards growing deployment of model-based methods to anticipate design problems and automate the development process. Delivering an unprecedented level of rigor, formal methods are gradually making their way into supporting tools for the development of aircraft systems. Nonetheless, there still remain compelling challenges to overcome to render formal methods widely applicable and accepted across the aerospace industry. This talk provides an overview of some of the opportunities and challenges encountered in introducing reactive synthesis methods to support the development of algorithms for the control of aircraft systems operations.

---

Adrian Francalanza

Extended Monitorability through Multiple Executions

Runtime Verification is a technique that uses monitors to analyse the execution of an executing system in order to determine whether a correctness property is satisfied or violated. Most of the work conducted in this field of research is limited to the analysis of a single system execution for teh verification of linear-time properties.

In this talk I will discuss recent work on investigating the increase in observational capabilities of monitors that analyse a system over multiple runs. I will illustrate how the augmented monitoring setup can affect the class of properties that can be verified at runtime focussing instead on branching-time properties expressed in the modal mu-calculus. Although branching-time properties are considered by many to be preserve of static verification techniques such as model-checking, our preliminary results show that the setup can be used to systematically extend previously established monitorability limits. If time permits, I will also discuss bounds that capture the correspondence between the syntactic structure of a branching-time property and the number of system runs required to conduct adequate runtime verification.

This is joint work with Antonis Achilleos and Jasmine Xuereb.

---

Bernhard Aichernig

Automata Learning and Testing in AALpy

In this talk I will discuss automata learning and its relation to black-box testing with the help of our AALpy tool (https://github.com/DES-Lab/AALpy).
This learning-based testing approach combines the active learning of finite-state models with model-based test-case generation. With AALpy we can learn (and test against) deterministic, non-deterministic, and stochastic models. Next to the automated testing of Python classes, we will cover more sophisticated applications, including protocol fuzzing (MQTT, Bluetooth, IPSec) and the mining of interpretable models from recurrent neural networks.

Chairmen

Dario Della Monica – Udine University, Italy
Ingo Pill – Silicon Austria Labs, Austria
Stefano Tonetta – Fondazione Bruno Kessler, Italy