1.8 KiB
(In)equivalences between systems hold because of different properties of the systems themselves. Logics = a formal way to express these properties.
- satisfiability relation states when a process satisfies a property
- enjoying the same properties coincides with being bisimilar
Example
These processes are not bisimilar as:
- P1 can perform an action a followed by any b
- P2, after every a, can always perform an action b
- so there exists an a after which P1 cannot perform a b. But not for P2
Syntax and Satisfiability
\phi := TT | \lnot \phi | \phi \land \phi|◇ a \phi \quad where a \in ActionThe language generated by this grammar will be denoted by Form; every element of this set will be called formula
To simplify the proofs, we consider a more general form of conjunction: \land_{i \in I, \phi_{i}}
where I is any indexing set (possibility, also infinite). Satisfiability for this operator is similar to that for the binary operator.
Of course, we can use the boolean constant FALSE (FF) and classical logical operators like disjunction \lor and implication => (they can all be derived in the usual way from TT, \lnot, \land).
Another very useful logical operator is "box": let us define \lnot \lozenge a p as \square a \lnot \phi
From the last condition, we have that $P \models \square a \phi if and only if \forall P': P \xrightarrow{a} P' \implies P' \models \phi
EXAMPLE: Let us now consider formula ☐aFF
By definition, this happens only if, for every P’ resulting from P after action a, it holds P’ |= FF
However, this can never happen, whatever P’ be; hence, P |= ☐aFF holds true only if P cannot perform any action a
