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

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

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

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

Cited in

(19)

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

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)