On-the-fly emptiness check of transition-based Streett automata

DOI10.1007/978-3-642-04761-9_17MaRDI QIDQ3648699zbMATH OpenOpenAlexFDO

Authors Alexandre Duret-Lutz, Denis Poitrenaud, Jean-Michel Couvreur

Publication date 1 December 2009

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Recommendations

• Model Checking Software
• Three SCC-based emptiness checks for generalized Büchi automata
• Generic emptiness check for fun and profit
• Strength-based decomposition of the property Büchi automaton for faster model checking
• Publication:4507820

Cites work

• Automata-Theoretic Model Checking Revisited
• Computer Aided Verification
• Depth-First Search and Linear Graph Algorithms
• Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning
• scientific article; zbMATH DE number 3862426 (Why is no real title available?)
• scientific article; zbMATH DE number 3972158 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1973991 (Why is no real title available?)
• scientific article; zbMATH DE number 1487477 (Why is no real title available?)
• scientific article; zbMATH DE number 1515289 (Why is no real title available?)
• scientific article; zbMATH DE number 1746645 (Why is no real title available?)
• scientific article; zbMATH DE number 1796123 (Why is no real title available?)
• Introduction to algorithms
• Modalities for model checking: Branching time logic strikes back
• Model Checking Software
• Nested emptiness search for generalized Büchi automata
• The Büchi Complementation Saga
• Verification by augmented abstraction: The automata-theoretic view

Cited in

(5)

• Determinization and limit-determinization of Emerson-Lei automata
• Abstraction refinement for emptiness checking of alternating data automata
• Generic emptiness check for fun and profit
• Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning
• Strength-based decomposition of the property Büchi automaton for faster model checking

Describes a project that uses

Uses Software

• SPOT
• LTL2BA

This page was built for publication: On-the-fly emptiness check of transition-based Streett automata

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