dc.contributor.author | Hermo Huguet, Montserrat | |
dc.contributor.author | Lucio Carrasco, Francisca | |
dc.contributor.author | Sánchez, César | |
dc.date.accessioned | 2024-02-08T08:35:34Z | |
dc.date.available | 2024-02-08T08:35:34Z | |
dc.date.issued | 2023-03-03 | |
dc.identifier.citation | Formal Methods : 495–513 (2023) | es_ES |
dc.identifier.isbn | 978-3-031-27480-0 | |
dc.identifier.uri | http://hdl.handle.net/10810/64905 | |
dc.description.abstract | We introduce a tableau decision method for deciding realizability of specifications expressed in a safety fragment of LTL that includes bounded future temporal operators. Tableau decision procedures for temporal and modal logics have been thoroughly studied for satisfiability and for translating temporal formulae into equivalent Büchi automata, and also for model checking, where a specification and system are provided. However, to the best of our knowledge no tableau method has been studied for the reactive synthesis problem.
Reactive synthesis starts from a specification where propositional variables are split into those controlled by the environment and those controlled by the system, and consists on automatically producing a system that guarantees the specification for all environments. Realizability is the decision problem of whether there is one such system.
In this paper, we present a method to decide realizability of safety specifications, from which we can also extract (i.e., synthesize) a correct system (in case the specification is realizable). The main novelty of a tableau method is that it can be easily extended to handle richer domains (integers, etc.) and bounds in the temporal operators in ways that automata approaches for synthesis cannot. | es_ES |
dc.description.sponsorship | This work was funded in part by the European Union (ERDF funds) under grant PID2020-112581GB-C22, European COST Action CA20111 EuroProofNet (European Research Network on Formal Proofs), by the University of the Basque Country under project LoRea GIU21/044, by the Madrid Regional Government under project S2018/TCS-4339 (BLOQUES-CM) and by a research grant from Nomadic Labs and the Tezos Foundation. | es_ES |
dc.language.iso | eng | es_ES |
dc.publisher | Springer | es_ES |
dc.rights | info:eu-repo/semantics/openAccess | es_ES |
dc.subject | safety specifications | es_ES |
dc.subject | synthesis | es_ES |
dc.subject | tableaux | es_ES |
dc.title | Tableaux for Realizability of Safety Specifications | es_ES |
dc.type | info:eu-repo/semantics/bookPart | es_ES |
dc.rights.holder | © 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG | * |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-031-27481-7_28 | |
dc.identifier.doi | 10.1007/978-3-031-27481-7 | |
dc.departamentoes | Lenguajes y sistemas informáticos | es_ES |
dc.departamentoeu | Hizkuntza eta sistema informatikoak | es_ES |