Compositional SCC analysis for language emptiness

DOI10.1007/s10703-006-4617-3zbMath1100.68059OpenAlexW2074669650MaRDI QIDQ2505627

Kavita Ravi, Roderick Bloem, Gary D. Hachtel, Fabio Somenzi, Chao Wang

Publication date: 28 September 2006

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-006-4617-3

zbMATH Keywords

model checkingabstraction refinementBDDLTLlanguage emptiness

Mathematics Subject Classification ID

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

Related Items (3)

Component-wise incremental LTL model checking ⋮ Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components ⋮ Survey on Directed Model Checking

Uses Software

• visualSTATE
• VIS

Cites Work

• An iterative approach to verification of real-time systems
• Testing language containment for \(\omega\)-automata using BDDs
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Graph-Based Algorithms for Boolean Function Manipulation
• Interpolants and Symbolic Model Checking
• Verification of large state/event systems using compositionality and dependency analysis
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Compositional SCC analysis for language emptiness