Symbolic bounded synthesis
From MaRDI portal
Publication:453535
DOI10.1007/s10703-011-0137-xzbMath1247.68163OpenAlexW2023329406MaRDI QIDQ453535
Publication date: 27 September 2012
Published in: Formal Methods in System Design (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10703-011-0137-x
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items
Graph Games and Reactive Synthesis, Compositional and symbolic synthesis of reactive controllers for multi-agent systems, Safraless LTL synthesis considering maximal realizability, Unnamed Item, Synthesizing adaptive test strategies from temporal logic specifications, Practical synthesis of reactive systems from LTL specifications via parity games, A symbolic algorithm for lazy synthesis of eager strategies
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Symbolic model checking: \(10^{20}\) states and beyond
- Model checking and boolean graphs
- Reasoning about infinite computations
- Binary decision diagrams in theory and practice
- A linear-time model-checking algorithm for the alternation-free modal mu- calculus
- SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA
- Bounded Synthesis
- Selective Approaches for Solving Weak Games
- Synthesis of Asynchronous Systems
- Solving Games Without Determinization
- An Antichain Algorithm for LTL Realizability
- Graph-Based Algorithms for Boolean Function Manipulation
- Branching Programs and Binary Decision Diagrams
- Compositional Algorithms for LTL Synthesis
- On Locally Checkable Properties
- Revisiting Synthesis of GR(1) Specifications
- From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
- Verification, Model Checking, and Abstract Interpretation
