ProcessAlgebra

  • Day1
    • Yoshiki explained why he needs encoding of process algebra; he plans to write a communication protocol as a term in process algebra and generate a set of possible sequences of atomic action which meets the term. In order to do it, he plans to write a calculator which, for a given term E in ACP (one of the equational theories in process algebra), gives a guarded term equivalent to E.
    • We had a sketch of a proof that such calculator exists; i.e., we showed, given an ACP term E, there is a sequence (a_i, E_i) of pairs of an atomic term a_i and a term E_i such that E is equivalent to Sigma_{i=1}^{i < N} a_i . E_i .
    • It seems straightforward to extract a calculator out of the (informal) proof of the above proposiion.
  • Day2
    • Nisse showed an old code for CBS(Prasad's) using mixed induction-coinduction.
    • Discussed where to use least and greatest fixed points. Nice explanation by Yoshiki wasn't bought by Nisse/Simon.
    • Algorithm for canonicalising ACP terms(expansion from parallel terms to sequential terms)
    • Writing down the proof of the above.
  • Day3 Y explained his interpretation of semantics to Martin. Became clear there are three relations between terms that shouldn't be confused.
    1. Eta equality ---> leading to ACP algebra
    2. Rewriting rel between the equiv class of terms ---> op.sem.
    3. Rewriting of parallel terms to sequential terms
    Y emphasis: 1 and 2 shouldn't be confused. (Mixed induction coinduction ...) (Presence or absence of infinite terms) (Y approach: finite terms + rewrite relation) (Nisse approach: infinite terms)
    Started implementing the 3rd rew. rules.
  • Day4: Implemented expansion from para terms to sequential terms.
  • Day5: The 1st goal (expansion) achieved. Vaguely thinking about semantics. Gathering material to be put in Agda Wiki, including Simon's expansion function and Nisse's CBS formalization.
Page last modified on September 07, 2010, at 02:19 pm
Powered by PmWiki