zbMATH — the first resource for mathematics

On the Herbrand-Kleene universe for nondeterministic computations. (English) Zbl 0567.68024
For nondeterministic recursive equations over an arbitrary signature of function symbols including the nondeterministic choice operator ”or” the interpretation is factorized according to the techniques developed earlier by the author. It is shown that one can either associate an infinite tree with the equations, then interpret the function symbol ”or” as a nondeterministic choice operator and so mapping the tree onto a set of infinite trees and then interpret these trees. Or one can interpret the recursive equation directly yielding a set-valued function. Both possibilities lead to the same result, i.e., one obtains a communication diagram. However, one has to use more refined techniques than just powerdomains. This explains and solves a problem posed by M. Nivat [Information processing, Proc. IFIP Congr., Tokyo and Melbourne 1980, 17- 28 (1980; Zbl 0444.68011)]. Basically, the construction gives a generalization of the powerdomain approach applicable to arbitrary nonflat (nondiscrete) algebraic domains.

68Q65 Abstract data types; algebraic specification
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI
[1] Broy, M., Fixed point theory for communication and concurrency, (), 125-147
[2] Broy, M.; Wirsing, M., Partial abstract types, Acta informatica, 18, 1, 47-64, (1982) · Zbl 0494.68020
[3] Nivat, M., On the intepretation of recursive polyadic program schemes, (), 255-281
[4] Nivat, M., Nondeterministic programs: an algebraic overview, (), 17-28
[5] Plotkin, G., A powerdomain construction, SIAM J. comput., 5, 452-486, (1976) · Zbl 0355.68015
[6] Smyth, M.B., Power domains, J. css, 16, 23-36, (1978) · Zbl 0391.68011
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.