Merging regular processes by means of fixed-point theory

concurrency correctness denotational semantics fair merge fairness infinite words interleaving Iteration Kleene-star iteration recursion semantics of processes trace theory while- statements

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Theory of operating systems (68N25)

Review text

First, we investigate a trace-set semantics of processes with \(\mu\)- recursion and arbitrary interleaving (merge). \(\mu\)-recursion is the analogue of recursion in standard programming by means of a recursive procedure. Iteration using while-statements can be viewed as a special case of this: so-called regular recursion. The semantics is used to support a formalism that determines the merge of two regular sequential (nondeterministic) processes. Next, we turn to processes with merge, \(\mu\)-recursion, and a second kind of recursion, called \(\alpha\)- recursion. This kind of recursion when applied in a regular forms is the equivalent of the Kleene-star iteration known from formal language theory. It involves only arbitrary big, but finite numbers of iterations. A different, more complicated framework is needed to give meaning to this kind of processes. Hereafter we define the semantics of the fair merge of these processes. Finally, we use this to prove the correctness of a formalism similar to the one for arbitrary merge in order to calculate the fair merge of two regular sequential (nondeterministic) processes with \(\mu\)-recursion.

Recommendations

Cites work

Cited in

(11)

This page was built for publication: Merging regular processes by means of fixed-point theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1082070)