×

zbMATH — the first resource for mathematics

A generalization of ACP using Belnap’s logic. (English) Zbl 1106.68075
Summary: ACP is combined with Belnap’s four-valued logic via conditional composition (if-then-else). We show that the operators of ACP can be seen as instances of more general, conditional operators. For example, both the choice operator + and \(\delta\) (deadlock) can be seen as instances of conditional composition, and the axiom \(x+\delta=x\) follows from this perspective. Parallel composition is generalized to the binary conditional merge \(_\varphi\|_\psi\) where \(\varphi\) covers the choice between interleaving and synchronization, and \(\psi\) determines the order of execution. The instance \({}_{\text{B}} \|_{\text{B}}\) is ACP’s parallel composition, where B (both) is the truth value that models both true and false in Belnap’s logic. Other instances of this conditional merge are sequential composition, pure interleaving and synchronous merge. We investigate the expression of scheduling strategies in the conditions of the conditional merge.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B50 Many-valued logic
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aceto, L.; Fokkink, W.J.; van Glabbeek, R.J.; Ingólfsdóttir, A., Axiomatizing prefix iteration with silent steps, Inform. and comput., 127, 1, 26-40, (1996) · Zbl 0855.68030
[2] Belnap, N.D., A useful four-valued logic, (), 8-37
[3] Bergstra, J.A.; Bethke, I.; Ponse, A., Process algebra with iteration and nesting, The computer journal, 37, 4, 243-258, (1994) · Zbl 0953.68572
[4] Bergstra, J.A.; Bethke, I.; Rodenburg, P.H., A propositional logic with 4 values: true, false, divergent and meaningless, J. appl. non-classical logics, 5, 2, 199-218, (1995) · Zbl 0843.03012
[5] Bergstra, J.A.; Klop, J.W., Process algebra for synchronous communication, Inform. and control, 60, 1/3, 109-137, (1984) · Zbl 0597.68027
[6] Bergstra, J.A.; Middelburg, C.A., A thread algebra with multi-level strategic interleaving, (), 35-48 · Zbl 1113.68426
[7] Bergstra, J.A.; Ponse, A., Kleene’s three-valued logic and process algebra, Inform. process. lett., 67, 2, 95-103, (1998) · Zbl 1338.68200
[8] Bergstra, J.A.; Ponse, A., Process algebra with four-valued logic, J. appl. non-classical logics, 10, 1, 27-53, (2000) · Zbl 1036.68067
[9] Bracha, G., The Java language specification, (2000), Addison Wesley
[10] Dijkstra, E.W., Cooperating sequential processes, (), 43-112
[11] Fitting, M.C., Kleene’s three valued logics and their children, Fund. inform., 20, 113-131, (1994) · Zbl 0804.03016
[12] van Glabbeek, R.J., A complete axiomatization for branching bisimulation congruence of finite-state behaviours, (), 473-484
[13] Jones, C.B., Systematic software development using VDM, (1990), Prentice-Hall International Englewood Cliffs · Zbl 0743.68048
[14] Kleene, S.C., On a notation for ordinal numbers, J. symbolic logic, 3, 150-155, (1938) · Zbl 0020.33803
[15] Kleene, S.C., Representation of events in nerve nets and finite automata, (), 3-41 · Zbl 0061.01003
[16] A. Ponse, M.B. van der Zwaag, The logic of ACP. Report SEN-R0207, CWI, 2002. Also appeared in: M.B. van der Zwaag, Models and Logics for Process Algebra, Ph.D. thesis, IPA Dissertation Series 2002-11, ISBN 90-5170-636-7, 2002.
[17] A. Ponse, M.B. van der Zwaag, ACP and Belnap’s Logic, in: Short Contributions from the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond, Bertinoro, Italy, August 2005. BRICS Notes Series NS-05-3, 2005.
[18] A. Ponse, M.B. van der Zwaag, Belnap’s logic and conditional composition, to appear in TCS. · Zbl 1179.03029
[19] Verhoef, C., A congruence theorem for structured operational semantics with predicates and negative premises, Nordic journal of computing, 2, 2, 274-302, (1995) · Zbl 0839.68060
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.