×

Readiness semantics for regular processes with silent actions. (English) Zbl 0646.68019

Automata, languages and programming, Proc. 14th Int. Colloq., Karlsruhe/FRG 1987, Lect. Notes Comput. Sci. 267, 115-125 (1987).
[For the entire collection see Zbl 0616.00013.]
The authors set out to define a process algebra with silent actions along with an appropriate readiness semantics. Silent actions are distinguished elements of the action vocabulary of a formal specification for regular processes. They represent constituents of an action sequence that are not controllable by the environment of the considered system, but introduce the possibility of non-deterministic state transitions.
A readiness model on a process algebra based on a given action vocabulary is an abstraction of a transition system with this vocabulary. The process algebra is carefully designed so as to facilitate its integration into an adequate logic specification language. At first the algebra of readiness models with silent actions is presented, followed by a concise presentation of an algebra for sequential processes along with its operational semantics. Then the notion of readiness semantics is applied to finitary and recursive terms for this process algebra. A complete axiomatization of readiness equivalence is outlined.
Finally readiness semantics for an algebra of regular communicating processes is developed. Terms of this algebra are either sequential processes or terms obtained by applying to sequential processes the operators of parallel composition, restriction and abstraction. As theory would have it, the combination of this process algebra with an expressive logic as specification formalism can often considerably simplify description and verification of processes.
Reviewer: R.Horsch

MSC:

68N25 Theory of operating systems
68Q60 Specification and verification (program logics, model checking, etc.)
68Q65 Abstract data types; algebraic specification

Citations:

Zbl 0616.00013