Sciweavers

ENTCS
2007

Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems

13 years 4 months ago
Process Algebra Having Inherent Choice: Revised Semantics for Concurrent Systems
Process algebras are standard formalisms for compositionally describing systems by the dependencies of their observable synchronous communication. In concurrent systems, parallel composition introduces resolvable nondeterminism, i.e., nondeterminism that will be resolved in later design phases or by the operating system. Sometimes it is also important to express inherent nondeterminism for equal (communication) labels. Here, we give operational and axiomatic semantics to a process algebra having a parallel operator interpreted as concurrent and having a choice operator interpreted as inherent, not only w.r.t. different, but also w.r.t. equal next-step actions. In order to handle the different kinds of nondeterminism, the operational semantics uses µ-automata as underlying semantical model. Soundness and completeness of our axiom system w.r.t. the operational semantics is shown.
Harald Fecher, Heiko Schmidt
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Where ENTCS
Authors Harald Fecher, Heiko Schmidt
Comments (0)