Strength-based decomposition of the property Büchi automaton for faster model checking

DOI10.1007/978-3-642-36742-7_42MaRDI QIDQ5326352zbMATH OpenOpenAlexFDO

Authors E. Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

Publication date 5 August 2013

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-36742-7_42

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Three SCC-based emptiness checks for generalized Büchi automata
• On-the-fly emptiness check of transition-based Streett automata
• Model Checking Software
• Comparison of algorithms for checking emptiness on Büchi automata
• Parallel Explicit Model Checking for Generalized Büchi Automata

Cited in

(3)

• Computing bottom SCCs symbolically using transition guided reduction
• scientific article; zbMATH DE number 1979546 (Why is no real title available?)
• On-the-fly emptiness check of transition-based Streett automata

Describes a project that uses

Uses Software

• SPIN
• BEEM

This page was built for publication: Strength-based decomposition of the property Büchi automaton for faster model checking

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