Divide and compose: SCC refinement for language emptiness

DOI10.1007/3-540-44685-0_31MaRDI QIDQ4791850zbMATH OpenFDO

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

Publication date 3 February 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2154/21540456.htm

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Compositional SCC analysis for language emptiness
• Sharp disjunctive decomposition for language emptiness checking
• Fixpoint Guided Abstraction Refinement for Alternating Automata
• Analysis of symbolic SCC hull algorithms
• Three SCC-based emptiness checks for generalized Büchi automata

Cited in

(4)

• GSTE is partitioned model checking
• Compositional SCC analysis for language emptiness
• Sharp disjunctive decomposition for language emptiness checking
• A truly symbolic linear-time algorithm for SCC decomposition

This page was built for publication: Divide and compose: SCC refinement for language emptiness

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