PROP | P | T | true |

F | false |
||

Q | agent variables (which may not be T or F) begin with upper case |
||

~P | negation | ||

P & P | conjunction |
||

P | P | disjunction |
||

(P) | you can use brackets just as you'd expect |
||

P => P | implication | ||

[a,...]P | strong necessity |
||

[-a,...]P | strong complement necessity |
||

[[a,...]]P | weak necessity | ||

[[-a,...]]P | weak complement necessity | ||

<a,...>P | strong possibility |
||

<-a,...>P | strong complement possibility |
||

<<a,...>>P | weak possibility | ||

<<-a,...>>P | weak complement possibility | ||

[S]P | strong necessity using a set identifier S | ||

[-S]P | strong complement necessity using a set identifier S | ||

[[S]]P | weak necessity using a set identifier S | ||

[[-S]]P | weak complement necessity using a set identifier S | ||

<S>P | strong possibility using a set identifier S | ||

<-S>P | strong complement possibility using a set identifier S | ||

<<S>>P | weak possibility using a set identifier S | ||

<<-S>>P | weak complement possibility using a set identifier S | ||

min(X.P) | least fixpoint temporal formula |
||

max(X.P) | greatest fixpoint temporal formula |
||

V(Q,...) | parameterised agent |

Edinburgh Concurrency Workbench (v7.1). Page generated: Sat Jul 17 22:16:15 BST 1999