Instantly share code, notes, and snippets.

# arijits17/gist:a5a4aa8c87ef410682cfc5ee49b19239 Last active Feb 14, 2018

## Traces

Independence alphabet:

(Sigma, I): I irreflexive and symmetric

Dependence relation: complement of I, reflexive and symmetric

One step equivalence: uabv <-> ubav for (a,b) in I

Trace equivalence: transitive closure of one step equivalence

w <=> w' if w = w1 <-> w2 <-> ... <-> wk = w'

Example:

(a,b) in I: aabb <=> bbaa because

aabb <-> abab <-> baab <-> baba <-> bbaa

• A trace is an equivalence class with respect to <=>

• [w] is the trace containing w: [w] = { w' | w <=> w' }
• L is trace consistent if w in L implies [w] subset of L

• Every trace is either completely in L or completely out of L
• A trace consistent language L is called a "trace language"

• A regular trace language is a trace language who underlying word language is regular in the usual sense

Traces as labelled partial orders:

• Better way of thinking of a trace

• (E,<=,l) where

• (E,<=) is a partial order, E is a finite set of events

• l: E -> Sigma is the labelling function

• (l(e),l(e')) in D iff e <= e' or e' <= e
• e immediately less than e' => (l(e),l(e')) in D
• The words in [w] are all the valid linearizations of the partial order corresponding to [w]

Trace language:

• Word language that is compatible with trace equivalence

• Regular trace language: trace language that is regular when viewed as set of strings

Trace prefix:

• For traces [w], [w'], [w] <= [w'] if [w'] "extends" [w].

• For some u in [w] and u' in [w'], u is a prefix of u'

• We call [w] a trace prefix of [w']

• Example: With (a,b) in I, [b] <= [ab] because b in [b] and ba in [ab] such that b is a prefix of ba

• In the partial order representation, [w] <= [w'] if the partial order [w'] extends that of [w]. In other words [w] is downward closed subset of [w'].

Constructing a canonical trace from a firing sequence:

• By induction build a net N_w = (P_w,T_w,F_w) and a marking M_w for each word w

• For each firing sequence wt extending wt, N_w is included in N_wt

• N_w is identical to N_w' for each w'<=>w : each concurrent run generates a canonical net

• If we "throw away" the places in N_w, we get a canonical partial order representation of the trace [w]

• Now [w] <= [w'] iff the N_w is a prefix of N_{w'}

• Causal net:

• Each place has at most one incoming and one outgoing edge
• F* is a acyclic (partial order)
• Transitions that are not ordered are concurrent

======================================================================