Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
By a prefix order we mean a partial order which is also downwards totally ordered.
The concept was introduced in (Cuijpers 13a, Cuijpers 13b) in the context of semantics for programming languages, and in particular hybrid and cyber-physical systems, as need arose to generalize the notion of (execution) tree to something that would include a mix of continuous and discrete progress of time. After a lot of experimentation, Cuijpers 13a discovered that the generalization needed was something that expresses two things: time branches when it goes forward (due to different possible courses of action a system may take), but seems linear when looking backward.
A different way of looking at it, is that executions of systems have a natural prefix order on them. Trying to come up with a generic definition of what a ‘prefix’ is, Cuijpers could not find anything in literature and came up with the definition below. As it turns out, in roughly the same period, Ferlez-Cleaveland-Marcus 14 discovered the definition of “pointed prefix orders” and named them “generalized execution trees”.
A prefix order may be understood as a set with extra structure.
Given a set , a prefix order on is a (binary) relation with the following properties:
reflexivity: always;
transitivity: if , then ;
antisymmetry: if , then .
downward totality: if and , then or .
A prefix ordered set is a set equipped with a prefix order.
A prefix ordered set is precisely a poset satisfying the extra condition that and implies that or .
The morphisms of prefix ordered sets are history preserving functions. Given , the history of is the set . A history preserving function from a prefix ordered set to a prefix ordered set is a function from to (seen as structured sets) such that .
Equivalently, it is a monotone function between and (interpreted as posets) satisfying the additional property that for every and such that there exists a with and .
In this way, prefix ordered sets form a category Pfx. Furthermore, they are sometimes also viewed as a concrete category over Pos (rather than Set), with history preserving maps preserving the way in which executions of a system unfold, while order preserving maps preserve only the way in which the executions are observed by external observers. (For an example of why this distinction is useful, see also the article on embedding open maps? as a generalization of bisimulation)
Every prefix order is isomorphic to its set of histories under subsets, leading to the intuition that the elements of a prefix order ‘are’ their histories. Formally: given a prefix ordered set , the set is prefix ordered and isomorphic to (with ‘taking the history of an element’ and ‘taking the maximum of a history’ being the witnessing isomorphisms).
Products of prefix orders are not the usual Cartesian products, but rather are formed by all possible ‘mergings’ of the histories of elements of the combined prefix orders.
In the work of Cleaveland, a different type of products was defined, but at this point I do not know of a notion of morphism on prefix ordered sets that would result in that product.
Pieter Cuijpers, Prefix Orders as a General Model of Dynamics, Proceedings of the 9th International Workshop on Developments in Computational Models (DCM) p. 25–29 (pdf)
Pieter Cuijpers, The Categorical Limit of a Sequence of Dynamical Systems, EPTCS 120 : Proceedings EXPRESS/SOS 2013, p. 78-92, 2013 (arXiv:1307.7445, doi:10.4204/EPTCS.120.7)
James Ferlez, Rance Cleaveland, Steve Marcus, Generalized Synchronization Trees, LLNCS 8412: Proceedings of FOSSACS’14, 2014, p. 304–319 (10.1007/978-3-642-54830-7_20)
Last revised on March 9, 2021 at 18:23:30. See the history of this page for a list of all contributions to it.