(2020) Explainable Reactive Synthesis.
|
Text
BFT20.pdf Download (532kB) | Preview |
Abstract
Reactive synthesis transforms a specification of a reactive system, given in a temporal logic, into an implementation. The main advantage of synthesis is that it is automatic. The main disadvantage is that the implementation is usually very difficult to understand. In this paper, we present a new synthesis process that explains the synthesized implementation to the user. The process starts with a simple version of the specification and a corresponding simple implementation. Then, desired properties are added one by one, and the corresponding transformations, repairing the implementation, are explained in terms of counterexample traces. We present SAT-based algorithms for the synthesis of repairs and explanations. The algorithms are evaluated on a range of examples including benchmarks taken from the SYNTCOMP competition.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Bernd Finkbeiner (Reactive Systems Group, RSG) |
| Conference: | ATVA International Symposium on Automated Technology for Verification and Analysis |
| Depositing User: | Bernd Finkbeiner |
| Date Deposited: | 04 Mar 2021 16:21 |
| Last Modified: | 11 May 2021 13:59 |
| Primary Research Area: | NRA2: Reliable Security Guarantees |
| URI: | https://publications.cispa.saarland/id/eprint/3380 |
Actions
Actions (login required)
 |
View Item |