master-degree-notes/Concurrent Systems/notes/15 - A formal language for LTSs.md

(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 Action

The 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

Let us now define the set of formulae satisfied by a process as L(P) = \{ \phi \in Form:P \models \phi \} To simplify the proof, let us modify the set of formulae by allowing conjunctions over a numerable set of formulae

Theorem P \sim Q \space iif \space L(P)=L(Q)

(=>) By induction on the syntax tree of the formula, let's show that φ∈L(P) \space iff \space φ∈L(Q) Base case: The only possible case is with φ = TT.

• by the satisfiability relation, \phi belongs to the set of formulae of every process
• so also to L(P) and L(Q)

Inductive step: Let's assume the thesis for every tree of height at most h. Let h+1 be the height of \phi. Let's distinguish on the outmost operator in \phi

(<=) We prove that R \triangleq \{ (P, Q) : L(P)=L(Q) \} is a simulation; this suffices, since the relation just defined is trivially symmetric (so is a bisimulation too).

Let (P, Q) \in R and P \xrightarrow{a} P'. Let's consider \phi \triangleq \lozenge a \phi' \space where \space \phi'\triangleq \bigwedge_{\phi'' \in L(P')}\phi'' By construction, P \models \phi, hence, Q \models \phi, because L(Q) = L(P); then, \exists Q' : Q \xrightarrow{a} Q' such that Q'\models \phi'. (quindi "deve esistere un Q' che fa almeno tutto quello che fa P'") We proven that the formulas satisfied by P' are all satisfied by Q'

Hence, \forall \phi'' \in L(P'), \space \phi'' \in L(Q'), \space i.e. \space L(P') \subseteq L(Q')

By contradiction, let us assume that the inclusion is a proper, i.e. L(P') \subset L(Q'). Thus, \exists \hat{\phi}:\hat{\phi}\in L(Q') \land \hat{\phi} \not \in L(P').

Then, \lnot \hat{\phi} \in L(P') and this would imply that \lnot \hat{\phi} \in L(Q'). This is a contradiction because L(Q') cannot contain a formula and its negation.