Logical Formulas

Safety Properties:

F ::= A[ ] P |

E<> P

Always P

P ::= Proc.l | x = n | v = n |

x<=n | x<n |

P and P | not P | P or P |

P implies P

Possibly P

where

atomic properties

Process Proc at location l

clock comparison

boolean combinations

Previous slide

Next slide

Back to first slide

View graphic version