A basic theory of labelled transition systems, (linear) traces and simulation relations.
In subsequent PRs we are going to reconcile LTS semantics (interleaving semantics) with pomset and event structure semantics (non-interleaving).
Two important lemmas proved in this PR are sim_lang and bisim_lang.
These lemmas assert that a language accepted by one LTS can also be accepted by another one if there exists a simulation (bisimulation) relation between the initial states (see the formal statement in the code).
A basic theory of labelled transition systems, (linear) traces and simulation relations. In subsequent PRs we are going to reconcile LTS semantics (interleaving semantics) with pomset and event structure semantics (non-interleaving). Two important lemmas proved in this PR are
sim_langandbisim_lang. These lemmas assert that a language accepted by one LTS can also be accepted by another one if there exists a simulation (bisimulation) relation between the initial states (see the formal statement in the code).