On Closure Operator for Interval Order Structures.
Conferences
Overview
Identity
Additional Document Info
View All
Overview
abstract
Formal studies of models of concurrency are usually focused on two major models: Interleaving abstraction (Bergstra, 2001; Milner, 1990) and partially ordered causality (Diekert and Rozenberg, 1995; Jensen, 1997; Reisig, 1998). Although very mature, these models retain a known limitation: Neither of them can model the “not later than” relationship effectively, which causes problems with specifying priorities, error recovery, time testing, inhibitor nets, etc. See for reference: Best and Koutny (1992); Janicki (2008); Janicki and Koutny (1995); Juhas et al. (2006); Kleijn and Koutny (2004).
A solution, proposed independently (in this order) in (Lamport, 1986; Gaifman and Pratt, 1987) and (Janicki and Koutny, 1991), suggests to model concurrent behaviours by an ordered structure, i.e. a triple (X, R1, R2), where X is the set of event occurrences, and R1 and R2 are two binary relations on X. The relation R1 is interpreted as “causality”, i.e. an abstraction of the “earlier than” relationship, and R2 is interpreted as “weak causality”, an abstraction of the “not later than” relationship.
For ordered structures’ model, the following two kinds of relational structures are of special importance: stratified order structures (SO-structures) and interval order structures (IO-structures). The SO-structures can fully model concurrent behaviours when system executions (operational semantics) are described in terms of stratified orders, while the IO-structures can fully model concurrent behaviours when system executions are described in terms of interval orders (Janicki, 2008; Janicki and Koutny, 1997). It was argued in (Janicki and Koutny, 1993), and also implicitly in a 1914 Wiener’s paper Wiener (1914), that any execution that can be observed by a single observer must be an interval order. Thus, IO-structures provide a very definitive model of concurrency. However, the theory of IO-structures remains far less developed than its simpler counterpart - the theory of SO-structures.
One of the most important concepts lying at the core of partial orders and algebraic structures theory is the concept of transitive closure of relations. The equivalent of transitive closure for SO-structures, called <>-closure, has been proposed in (Janicki and Koutny, 1995) and consequently used in (Janicki and Koutny, 1995; Juhas et al., 2006; Kleijn and Koutny, 2004) and others. However, a similar concept for IO-structures has not been proposed. In this thesis we define that concept.
We introduce the transitive closure for IO-structures, called the []-closure. We prove that it has same properties as the standard transitive closure for partial orders and []-closure for SO-structures (published in Janicki and Zubkova (2009); Janicki et al. (2009)), and provide some comparison of different versions of transitive closure used in various relational structures. Some properties of another recently introduced *-closure (Janicki et al., 2013) are also discussed.
