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.

Edit | History | Recent Changes (all) | Search

Page last modified on September 07, 2010, at 02:19 pm