2003
Efficient Model Checking of Safety Properties
- Year
- 2003
- Authors
- Timo Latvala
- Venue
- SPIN 2003 / LNCS 2648
- Keywords
- LTL, safety properties, finite automata
Abstract
. We consider the problems of identifying LTL safety proper- ties and translating them to finite automata. We present an algorithm for constructing a finite automata recognising informative prefixes of LTL formulas based on [1]. The implementation also includes a procedure for deciding if a formula is pathologic. Experimental results indicate that the translation is competitive when compared to model checking with tools translating full LTL to Büchi automata.