master-degree-notes/Concurrent Systems/notes/14.md

We shall only consider finite processes (processes without recursive definitions)

• a limited handling of recursion is possible
• deciding bisimilarity for general processes is undecidable

Inference system = axioms + inference rules

• soundness: whatever I infer is correct (i.e., bisimiar)
• completeness: whatever is bisimilar, it can be inferred

Axioms & Rules for Strong Bisimilarity