Reference. Model Checking of Safety Properties [kupferman-vardi-2001]

November 2001
Orna Kupferman, Moshe Vardi
Formal Methods in System Design 19 291–314
10.1023/A:1011254632723

Backlinks

Definition. Bad prefixes [ltp-000B]

(from Model Checking of Safety Properties)

For a property $P$ , the bad prefixes of $P$ are those finite prefixes $t \in \Sigma ^\ast$ from which the violation of $P$ can be established, i.e. $\forall \sigma \in \Sigma ^\omega .\ t\sigma \notin P$ .

A property $P$ is a safety property iff all violating behaviours are extensions of bad prefixes.

Definition. Good prefixes [ltp-000D]

(from Model Checking of Safety Properties)

For a property $P$ , the good prefixes of $P$ are those finite prefixes $t \in \Sigma ^\ast$ from which the satisfaction of $P$ can be established, i.e. $\forall \sigma \in \Sigma ^\omega .\ t\sigma \in P$ .

A property $P$ is a guarantee property iff all satisfying behaviours are extensions of good prefixes.

Related

Journal. Formal Methods in System Design [fmsd]

https://link.springer.com/journal/10703

Formal Methods in System Design is a journal dedicated to presenting the latest advancements in formal methods for hardware and software system design.