Boolean abstractions for realizability modulo theories

DOI10.1007/978-3-031-37709-9_15MaRDI QIDQ6535690zbMATHFDO

Authors Andoni Rodríguez, César Sánchez

Publication date 1 February 2024

Mathematics Subject Classification ID

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

Recommendations

• Realizability of real-time logics
• Tableaux for realizability of safety specifications
• Boolean Abstraction for Temporal Logic Satisfiability
• An Antichain Algorithm for LTL Realizability
• Verification, Model Checking, and Abstract Interpretation

Cites work

• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 3408928 (Why is no real title available?)
• An automata-theoretic approach to constraint LTL
• Automata, logics, and infinite games. A guide to current research
• Bounded Synthesis
• Church’s Problem and a Tour through Automata Theory
• Counting minimal unsatisfiable subsets
• Fast, flexible MUS enumeration
• LTL with arithmetic and its applications in reasoning about hierarchical systems
• Synthesis of Reactive(1) designs
• Temporal stream logic modulo theories
• Temporal stream logic: synthesis beyond the Bools
• Temporal verification of reactive systems: response
• Vacuity in synthesis
• Verification, Model Checking, and Abstract Interpretation

Cited in

(1)

• Realizability modulo theories

This page was built for publication: Boolean abstractions for realizability modulo theories

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