Symbolic bounded synthesis

DOI10.1007/S10703-011-0137-XzbMATH Open1247.68163OpenAlexW2023329406MaRDI QIDQ453535FDOQ453535

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

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

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)

Cites Work

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

Cited In (12)

• Practical synthesis of reactive systems from LTL specifications via parity games
• Restriction of search space in systems of symbol processing
• Title not available (Why is that?)
• Bounded Synthesis
• Compositional and symbolic synthesis of reactive controllers for multi-agent systems
• Balancedness and coboundaries in symbolic systems
• Bounded Cycle Synthesis
• Graph Games and Reactive Synthesis
• Safraless LTL synthesis considering maximal realizability
• A symbolic algorithm for lazy synthesis of eager strategies
• Synthesizing adaptive test strategies from temporal logic specifications
• Unbeast: Symbolic Bounded Synthesis

Uses Software

• NuSMV
• CUDD
• LTL2BA

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)