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.

Proving unequivalences

The Logic approach presented so far is very natural for proving unequivalences:

• show one formula that is satisfied by a proc but not by the other

It is not very effective for concretely proving equivalences:

• e.g. to show that P \sim Q, we should check that every formula in L(P) belongs to L(Q) and conversely
• the problem is that L(P) is infinite, for every P, it contains TT, TT^TT, TT^TT^TT, ...
• even if we restrict to logical equivalence class, the situation does not change
• EXAMPLE: consider process P2
  • it satisfies ☐bFF, ☐cFF, ☐dFF, ...
  • so L(P2) is infinite because so is the action set

Sub-Logics

Let's consider the sub-logic without negation: \phi := TT | \phi \land \phi|◇ a \phi \quad where a \in Action Remark: the formula ☐aFF is not expressible anymore. Hence, we can only express through formulae what a process is able to do.

Let's call L(P) the set of negation-free formulae satisfied by process P.

Theorem

P simulates Q if and only if L(Q) \subseteq L(P)

Proof: The proof is similar to the one for the previous Theorem. The main difference is in the (⇐) implication, when φ = ⋄aφ′, because here we do not prove that the inclusion cannot be proper (indeed, in general it is not).

An easy corollary of this result is that there is a double simulation between P and Q if and only if L¬(P) = L¬(Q).

Example: it can be checked that L(P2) = L(P1) indeed, P1 can simulate P2 and viceversa, but the simulations are not bisimulations.