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

model checkingrealizabilitysafety specificationssynthesistableauxtemporal logic

Mathematics Subject Classification ID

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

Review text

The paper is interested in model checking a fragment of linear-time temporal logic. To this end the authors develop a tableau system based on a new normal form for logical formulas. They consider synthesis and realizability properties. In a tableau we must develop both Boolean connectives and modalities. Usually, tableaux address the satisfiability problem for a formula. The tableau is seen as a game between the system and the environment. The terse normal form is designed to work well in this game. Realizability of a formula means that the system has a winning strategy in the game. Realizability is more complex than usual satisfiability for linear-time temporal logic: we have 2-EXPTIME completeness versus PSPACE completeness. However, the emphasis is on safety formulas, since safety is a behavior useful in practice (nothing bad can happen). The work is relevant for robotics specifications.

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

• 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
• scientific article; zbMATH DE number 1189110 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• 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)