Stubborn Sets for Model Checking the EF/AG Fragment of CTL

The general stubborn set approach to CTL model checking 2] has the drawback that one either nds a stubborn set with only one enabled transition or one has to expand all enabled transitions. This restriction does not apply in our approach to a fragment of CTL. Furthermore, our reduction does not depend on the invisibility of transitions in a stubborn set.

• Type: Journal
• Year: 2000
• Where: FUIN
• Authors: Karsten Schmidt 0004
• Keywords: CTL Model, FUIN 2000, General, Stubborn Set