Symbolic bounded synthesis

DOI10.1007/S10703-011-0137-XMaRDI QIDQ453535zbMATH OpenOpenAlexFDO

Authors Rüdiger Ehlers

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

zbMATH Keywords

binary decision diagramssafety gamesbounded synthesisSafraless synthesissynthesis from LTL

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

Recommendations

• Bounded Synthesis
• Unbeast: Symbolic Bounded Synthesis
• Encodings of bounded synthesis
• A Symbolic Algorithm for the Synthesis of Bounded Petri Nets
• Symbolic bisimulations
• An optimized symbolic bounded model checking engine
• Towards specifying symbolic computation

Cites work

• scientific article; zbMATH DE number 1670772 (Why is no real title available?)
• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 1903345 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 2102704 (Why is no real title available?)
• A linear-time model-checking algorithm for the alternation-free modal mu- calculus
• An Antichain Algorithm for LTL Realizability
• Binary decision diagrams in theory and practice
• Bounded Synthesis
• Branching Programs and Binary Decision Diagrams
• Compositional algorithms for LTL synthesis
• From Nondeterministic B\"uchi and Streett Automata to Deterministic Parity Automata
• Graph-Based Algorithms for Boolean Function Manipulation
• Model checking and boolean graphs
• On Locally Checkable Properties
• Reasoning about infinite computations
• Revisiting Synthesis of GR(1) Specifications
• SYMBOLIC IMPLEMENTATION OF ALTERNATING AUTOMATA
• Selective Approaches for Solving Weak Games
• Solving Games Without Determinization
• Symbolic computational techniques for solving games
• Symbolic model checking: \(10^{20}\) states and beyond
• Synthesis of Asynchronous Systems
• Verification, Model Checking, and Abstract Interpretation

Cited in

(17)

• Unbeast: Symbolic Bounded Synthesis
• Temporal synthesis for bounded systems and environments
• Practical synthesis of reactive systems from LTL specifications via parity games
• Restriction of search space in systems of symbol processing
• Compositional and symbolic synthesis of reactive controllers for multi-agent systems
• Bounded Synthesis
• Balancedness and coboundaries in symbolic systems
• Bounded Cycle Synthesis
• Graph Games and Reactive Synthesis
• Bounded synthesis for Streett, Rabin, and \(\mathrm{CTL}^*\)
• Safraless LTL synthesis considering maximal realizability
• Encodings of bounded synthesis
• Approximating optimal bounds in prompt-LTL realizability in doubly-exponential time
• Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
• A symbolic algorithm for lazy synthesis of eager strategies
• Taming large bounds in synthesis from bounded-liveness specifications
• Synthesizing adaptive test strategies from temporal logic specifications

Describes a project that uses

Uses Software

• LTL2BA
• CUDD
• NuSMV

This page was built for publication: Symbolic bounded synthesis

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