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