The main contribution of this PR is the notion of the scheduling of lposet and pomset.
A schedule of labelled poset is a set of its totally ordered extensions. Scheduling of a pomset is a union of these extensions for each of the posets belonging to the pomset. Scheduling will be used later to connect pomset semantics with trace semantics.
The main proven lemmas are schedule_hom, scheduling_unistronger and scheduling_stronger which describe how schedulings of lposets and pomsets behave with respect to homomorphisms.
An auxiliary very helpful notion developed in this PR is Ext --- an extension of lposetp by another lposetq under the assumption that there exists a homomorphism from p to q (or in other words, the order in q should not contradict the order in p).
The main contribution of this PR is the notion of the scheduling of
lposetandpomset. A schedule of labelled poset is a set of its totally ordered extensions. Scheduling of a pomset is a union of these extensions for each of the posets belonging to the pomset. Scheduling will be used later to connect pomset semantics with trace semantics.The main proven lemmas are
schedule_hom,scheduling_unistrongerandscheduling_strongerwhich describe how schedulings oflposetsandpomsetsbehave with respect to homomorphisms.An auxiliary very helpful notion developed in this PR is
Ext--- an extension oflposetpby anotherlposetqunder the assumption that there exists a homomorphism fromptoq(or in other words, the order inqshould not contradict the order inp).