Unbeast: Symbolic Bounded Synthesis

DOI10.1007/978-3-642-19835-9_25MaRDI QIDQ3000656zbMATH OpenOpenAlexFDO

Authors Rüdiger Ehlers

Publication date 19 May 2011

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-19835-9_25

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• Symbolic bounded synthesis
• Lectures on Concurrency and Petri Nets
• Bounded Synthesis
• scientific article; zbMATH DE number 1903357
• Encodings of bounded synthesis
• Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables

Cites work

• An Antichain Algorithm for LTL Realizability
• Bounded Synthesis
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• Model checking of safety properties

Cited in

(19)

• The complexity of counting models of linear-time temporal logic
• Linear temporal logic -- from infinite to finite horizon
• Practical synthesis of reactive systems from LTL specifications via parity games
• Synthesis of succinct systems
• Can we build it: formal synthesis of control strategies for cooperative driver assistance systems
• Unisex: A unix-based symbolic executor for pascal
• Efficient trace encodings of bounded synthesis for asynchronous distributed systems
• Encodings of bounded synthesis
• Bounded Synthesis
• Symbolic bounded synthesis
• scientific article; zbMATH DE number 7455737 (Why is no real title available?)
• scientific article; zbMATH DE number 7278100 (Why is no real title available?)
• Unbeast
• High-level representation of benchmark families for Petri games
• Real-time policy enforcement with metric first-order temporal logic
• Tableaux for realizability of safety specifications
• Synthesis of compact strategies for coordination programs
• Symbolic solution of Emerson-Lei games for reactive synthesis
• Towards an efficient implementation of a tableau method for reactive safety specifications

Describes a project that uses

Uses Software

• LTL2BA
• CUDD
• NuSMV

This page was built for publication: Unbeast: Symbolic Bounded Synthesis

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