Tableaux for realizability of safety specifications

DOI10.1007/978-3-031-27481-7_28zbMath1529.68159arXiv2206.01492OpenAlexW4323026598MaRDI QIDQ6174549

Paqui Lucio, César Sánchez, Montserrat Hermo

Publication date: 17 August 2023

Published in: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2206.01492

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Synthesis of Reactive(1) designs
• The foundations of mathematics. A study in the philosophy of science
• Dual systems of tableaux and sequents for PLTL
• Reasoning about infinite computations
• Reducing bounded realizability analysis to reachability checking
• Practical synthesis of reactive systems from LTL specifications via parity games
• Lazy Synthesis
• Towards Efficient Parameterized Synthesis
• SAT-Based Synthesis Methods for Safety Specs
• Unbeast: Symbolic Bounded Synthesis
• Bounded Synthesis for Petri Games
• Bounded Synthesis
• Bounded Cycle Synthesis
• An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability
• Solving Sequential Conditions by Finite-State Strategies
• Verification, Model Checking, and Abstract Interpretation