Beyound SafetyDecoration

TACAS98

l

n

Leadsto:

Whenever l is reached

then n is reached with t

l

n

Decoration

new clock X

boolean B

X:=0

B:=tt

B:=ff

A[] (B implies x<=t)

Previous slide

Next slide

Back to first slide

View graphic version