Go backward to Conditional Implementation
Go up to Top
Go forward to Machine Closure
Safety and Closure
- Finite behavior
- Finite sequence of states.
- Formula , finite behavior rho.
- rho satisfies iff rho can be extended to infinite behavior
that satisfies .
- <> satisfies every behavior.
- Safety property
- Formula that is satisfied by infinite behavior sigma iff it is
satisfied by every prefix f sigma.
- and always [A] is a safety property.
- Closure
- A() = closure of .
- sigma satisfies A() iff every prefix of
sigma satisfies .
- Strongest safety property such that
|= A()
Wolfgang.Schreiner@risc.uni-linz.ac.at
Id: spec1.tex,v 1.1 1996/05/13 09:04:04 schreine Exp schreine