Towards an efficient implementation of a tableau method for reactive safety specifications

DOI10.1016/J.JLAMP.2024.101003MaRDI QIDQ6643466zbMATH OpenFDO

Authors Ander Alonso, M. Hermo, Josu Oca

Publication date 26 November 2024

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.JLAMP.2024.101003

zbMATH Keywords

synthesismodel checkingrealizabilitytemporal logictableauxsafety specifications

Mathematics Subject Classification ID

Applications of game theory (91A80) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• Tableaux for realizability of safety specifications
• An improved on-the-fly tableau construction for a real-time temporal logic.
• A tableau construction for finite linear-time temporal logic
• A tableau for temporal logic over the reals
• scientific article; zbMATH DE number 1696514

Cites work

• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• A first-order logic characterization of safety and co-safety languages
• Characterization of temporal property classes
• Complexity of DNF minimization and isomorphism testing for monotone formulas
• Dual systems of tableaux and sequents for PLTL
• LTL reactive synthesis with a few hints
• Model checking of safety properties
• Solving Sequential Conditions by Finite-State Strategies
• Synthesis of Reactive(1) designs
• Tableaux for realizability of safety specifications
• Temporal logic can be more expressive
• Unbeast: Symbolic Bounded Synthesis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Preface to selected papers from 22nd workshop on programming and languages (PROLE 2023)

This page was built for publication: Towards an efficient implementation of a tableau method for reactive safety specifications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6643466)