Instantly share code, notes, and snippets.

Embed
What would you like to do?

Concurrency Theory: Lecture 6, 06 February 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

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment