On the Construction of Fine Automata for Safety Properties

12 years 5 months ago
On the Construction of Fine Automata for Safety Properties
Of special interest in formal verification are safety properties, which assert that the system always stays within some allowed region. Each safety property can be associated with a set of bad prefixes: a set of finite computations such that an infinite computation violates iff it has a prefix in the set. By translating a safety property to an automaton for its set of bad prefixes, verification can be reduced to reasoning about finite words: a system is correct if none of its computations has a bad prefix. Checking the latter circumvents the need to reason about cycles and simplifies significantly methods like symbolic fixed-point based verification, bounded model checking, and more. A drawback of the translation lies in the size of the automata: while the translation of a safety LTL formula to a nondeterministic B
Orna Kupferman, Robby Lampert
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where ATVA
Authors Orna Kupferman, Robby Lampert
Comments (0)