CINECA IRIS Institutional Research Information System
IRIS è la piattaforma adottata dall’Università degli Studi di Udine per gestire l’archivio aperto dei prodotti della ricerca. L’archivio contiene articoli, contributi in volume, monografie, interventi pubblicati in atti di convegno, Tesi di dottorato e altri materiali.
EnglishRealizability and reactive synthesis from temporal logics are fundamental problems in the formal verification field. The complexity of the Linear-time Temporal Logic with Past (LTL+P) case led to the definition of fragments with lower complexities and simpler algorithms. Recently, the logic of Extended Bounded Response LTL+P (LTLEBR+ P ) has been introduced. It allows one to express any safety language definable in LTL and it is provided with an efficient, fully-symbolic algorithm for reactive synthesis. In this paper, we extend LTLEBR+ P with fairness conditions, assumptions, and guarantees. The resulting logic, called GR-EBR, preserves the main strength of LTLEBR+ P, that is, efficient realizability, and makes it possible to specify properties beyond safety. We study the problem of reactive synthesis for GR-EBR and devise a fully-symbolic algorithm that reduces it to a number of safety subproblems. To ensure soundness and completeness, we propose a general framework for safety reductions in the context of realizability of (fragments of) LTL+P. The experimental evaluation shows the feasibility of the approach.
| Titolo: | Fairness, Assumptions, and Guarantees for Extended Bounded Response LTL+P Synthesis | |
| Autori: | ||
| Data di pubblicazione: | 2021 | |
| Serie: | ||
| Abstract: | Realizability and reactive synthesis from temporal logics are fundamental problems in the formal verification field. The complexity of the Linear-time Temporal Logic with Past (LTL+P) case led to the definition of fragments with lower complexities and simpler algorithms. Recently, the logic of Extended Bounded Response LTL+P (LTLEBR+ P ) has been introduced. It allows one to express any safety language definable in LTL and it is provided with an efficient, fully-symbolic algorithm for reactive synthesis. In this paper, we extend LTLEBR+ P with fairness conditions, assumptions, and guarantees. The resulting logic, called GR-EBR, preserves the main strength of LTLEBR+ P, that is, efficient realizability, and makes it possible to specify properties beyond safety. We study the problem of reactive synthesis for GR-EBR and devise a fully-symbolic algorithm that reduces it to a number of safety subproblems. To ensure soundness and completeness, we propose a general framework for safety reductions in the context of realizability of (fragments of) LTL+P. The experimental evaluation shows the feasibility of the approach. | |
| Handle: | http://hdl.handle.net/11390/1217378 | |
| ISBN: | 978-3-030-92123-1 978-3-030-92124-8 | |
| Appare nelle tipologie: | 4.1 Contributo in Atti di convegno |
File in questo prodotto:
Copyright © 2022