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

DOI10.1007/978-3-642-36742-7_42zbMATH Open1381.68133OpenAlexW40595619MaRDI QIDQ5326352FDOQ5326352

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

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

Mathematics Subject Classification ID

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

Cited In (3)

• Computing bottom SCCs symbolically using transition guided reduction
• Title not available (Why is that?)
• On-the-fly emptiness check of transition-based Streett automata

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)