- Finite behavior
- Finite sequence of states.
- Formula $F$, finite behavior
`rho`. `rho`satisfies $F$ iff`rho`can be extended to infinite behavior that satisfies $F$.- <> satisfies every behavior.

- Safety property
- Formula that is satisfied by infinite behavior
`sigma`iff it is satisfied by every prefix f`sigma`. - $Init$
*and*`always`[`A`]$$_{v}is a safety property.

- Formula that is satisfied by infinite behavior
- Closure
`A`($F$) = closure of $F$.`sigma`satisfies`A`($F$) iff every prefix of`sigma`satisfies $F$.- Strongest safety property such that

|= $F$ $=>$`A`($F$)

Wolfgang.Schreiner@risc.uni-linz.ac.at

$$Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine $$