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}