Abstract
In this paper, we show that the non-deterministic choice “+”, which was proposed as a primitive operator in Synchronization Tree Logic (STL for short) can be defined essentially by conjunction and disjunction in the μ-calculus (μM for short). This is obtained by extending the μ-calculus with the non-deterministic choice “+” (denoted by μM + ) and then showing that μM + can be translated into μM. Furthermore, we also prove that STL can be encoded into μM + and therefore into μM.
Keywords
Download to read the full chapter text
Chapter PDF
References
Aceto, L., Hennessy, M.: Termination, deadlock, and divergence. Journal of ACM 39(1), 147–187 (1992)
Graf, S., Sifakis, J.: A logic for the description of non-deterministic programs and their properties. Information and Control 68, 254–270 (1986)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of ACM 32, 137–161 (1985)
Kozen, D.: Results on the propositional mu-calculus. Theoretical Computer Science 27, 333–354 (1983)
Larsen, K.G., Thomsen, B.: A modal process logic. In: The proc. of LICS 1988, pp. 203–210. IEEE Computer Science Society, Los Alamitos (1988)
Milner, R.: A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences 28, 439–466 (1984)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)
Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pacific J. Math. 5, 285–309 (1955)
Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional Mucalculus. Information and Computation 157, 142–182 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 IFIP International Federation for Information Processing
About this paper
Cite this paper
Zhan, N., Majster-Cederbaum, M. (2005). Deriving Non-determinism from Conjunction and Disjunction. In: Wang, F. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2005. FORTE 2005. Lecture Notes in Computer Science, vol 3731. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562436_26
Download citation
DOI: https://doi.org/10.1007/11562436_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29189-3
Online ISBN: 978-3-540-32084-5
eBook Packages: Computer ScienceComputer Science (R0)