Action Refinement in Process Algebras
Dr. Aceto studies the notion of action refinement in the setting of process description languages, together with behavioral equivalences for them and their associated proof systems. The presentation is organized into three parts. In the first, a semantic theory of processes based on atomic actions is used to give results that serve as a stepping stone toward the more complex theories needed to support action refinement. The core of the book then develops suitable notions of process equivalence for increasingly complex languages with operators for action refinement. This approach is used to highlight the difficulties introduced by synchronization among actions and scoping operators. In the final part, the author deals with the possibility of using action refinement to "observe" indirectly the causal relationships among actions in a system. A preliminary semantic theory for concurrent systems that relates concurrency and nondeterminism without reducing the former to the latter is also studied in some detail.
What people are saying - Write a review
We haven't found any reviews in the usual places.
A-posets abstract with respect apply the inductive Assume atomic actions axioms behavioural preorder binary relation bisimulation equivalence chapter clause coincide Comp completeness theorem completes the proof computations configurations congruence considered Corollary Cpar Cseq deadlock defined definition denotational semantics easy equivalence relation exists fact finitely approximable following lemma fully abstract given Hence HRFpar inductive hypothesis interleaving Intuitively labelled action refinement labelled processes labelled transition system LAct(A lemma modulo Moreover notation notion of equivalence obtain occurs operational semantics parallel composition Petri Nets Pos[A presented preserved by action process algebra properties Proposition prove q implies recx RECz red(p refine bisimulation refinement theorem result satisfies semantic equivalence semantic theory seq-prime sequential composition series-parallel pomsets standard statement strong bisimulation structural induction substitution syntactic termination predicate thai transition relations un(c wlog