(2021) Reactive Synthesis Beyond Realizability (Invited Tutorial).
|
Text
fmcad.pdf Download (81kB) | Preview |
Abstract
The automatic synthesis of reactive systems from high-level specifications is a highly attractive and increasingly viable alternative to manual system design, with applications in a number of domains such as robotic motion planning, control of autonomous systems, and development of communication protocols. The idea of asking the system designer to describe what the system should do instead of how exactly it does it holds a great promise. However, providing the right formal specification of the desired behavior of a system is a challenging task in itself. In practice it often happens that the system designer provides a specification that is unrealizable, that is, there is no implementation that satisfies it. Such situations typically arise because the desired behavior represents a trade-off between multiple conflicting requirements, or because crucial assumptions about the environment in which the system will execute are missing. Addressing such scenarios necessitates a shift towards synthesis algorithms that utilize quantitative measures of system correctness. In this tutorial, I will discuss two recent advances in this research direction. First, I will talk about the maximum realizability problem, where the input to the synthesis algorithm consists of a hard specification that must be satisfied by the synthesized system, and soft specifications which describe other desired, possibly prioritized properties, whose violation is acceptable. I will present a synthesis algorithm that maximizes a quantitative value associated with the soft specifications while guaranteeing the satisfaction of the hard specification. In the second half of the tutorial, I will present algorithms for synthesis in bounded environments, where a bound is associated with the sequences of input values produced by the environment. More concretely, these sequences consist of an initial prefix followed by a finite sequence repeated infinitely often, and satisfy the constraint that the sum of the lengths of the initial prefix and the loop does not exceed a given bound. I will also discuss the synthesis of approximate implementations from unrealizable specifications, which are guaranteed to satisfy the specification on at least a specified portion of the bounded-size input sequences. I will conclude by outlining some of the open avenues and challenges in quantitative synthesis from temporal logic specifications.
| Item Type: | Other |
|---|---|
| Divisions: | Rayna Dimitrova (RD) |
| Conference: | FMCAD Formal Methods in Computer-Aided Design |
| Depositing User: | Rayna Dimitrova |
| Date Deposited: | 11 May 2022 12:57 |
| Last Modified: | 11 May 2022 12:57 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3686 |
Actions
Actions (login required)
 |
View Item |