Abstract
Weak omega algebra and demonic refinement algebra are two ways of describing systems with finite and infinite iteration. We show that these independently introduced kinds of algebras can actually be defined in terms of each other. By defining modal operators on the underlying weak semiring, that result directly gives a demonic refinement algebra of commands. This yields models in which extensionality does not hold. Since in predicate-transformer models extensionality always holds, this means that the axioms of demonic refinement algebra do not characterise predicate-transformer models uniquely. The omega and the demonic refinement algebra of commands both utilise the convergence operator that is analogous to the halting predicate of modal μ-calculus. We show that the convergence operator can be defined explicitly in terms of infinite iteration and domain if and only if domain coinduction for infinite iteration holds.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Back, R.J., von Wright, J.: Refinement calculus: a systematic introduction. Springer, Heidelberg (1998)
Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J. (eds.) MPC 2000. LNCS, vol. 1837, pp. 45–59. Springer, Heidelberg (2000)
De Carufel, J.-L., Desharnais, J.: Demonic algebra with domain. In: Schmidt, R., Struth, G. (eds.) RelMiCS/AKA 2006. LNCS, vol. 4136, pp. 120–134. Springer, Heidelberg (2006)
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. Technical Report 2003-7, Universität Augsburg, Institut für Informatik, Revised version to appear in ACM TOCL (2003)
Desharnais, J., Möller, B., Struth, G.: Termination in modal Kleene algebra. In: Lévy, J.-J., Mayr, E., Mitchell, J. (eds.) Exploring new frontiers of theoretical informatics. IFIP International Federation for Information Processing Series, vol. 155, pp. 653–666. Kluwer, Dordrecht (2004)
Dijkstra, R.M.: Computation calculus bridging a formalisation gap. Science of Computer Programming 37, 3–36 (2000)
Guttmann, W., Möller, B.: Modal design algebra. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 236–256. Springer, Heidelberg (2006)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)
Hoare, C.A.R., He, J.: Unifying theories of programming. Prentice-Hall, Englewood Cliffs (1998)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)
Kozen, D.: Kleene algebra with tests. ACM Transactions on Programming Languages and Systems 19, 427–443 (1997)
Möller, B.: Lazy kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004); Revised version: B. Möller: Kleene getting lazy. Sci. Comput. Prog. (to appear)
Möller, B., Struth, G.: Modal Kleene algebra and partial correctness. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 379–393. Springer, Heidelberg (2004); Revised and extended version: B. Möller, G. Struth: Algebras of modal operators and partial correctness. Theoretical Computer Science 351, 221–239 (2006)
Möller, B., Struth, G.: wp is wlp. In: MacCaull, W., Winter, M., Düntsch, I. (eds.) RelMiCS 2005. LNCS, vol. 3929, pp. 200–211. Springer, Heidelberg (2006)
Morgan, C.: Data Refinement by Miracles. Inf. Process. Lett. 26, 243–246 (1988)
Morris, J.M.: Laws of data refinement. Acta Informatica (26), 287–308 (1989)
Nelson, G.: A generalization of Dijkstra’s calculus. ACM TOPLAS 11, 517–561 (1989)
Solin, K., von Wright, J.: Refinement algebra with operators for enabledness and termination. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 397–415. Springer, Heidelberg (2006)
von Wright, J.: From kleene algebra to refinement algebra. In: Boiten, E.A., Möller, B. (eds.) MPC 2002. LNCS, vol. 2386, pp. 233–262. Springer, Heidelberg (2002)
von Wright, J.: Towards a refinement algebra. Sci. Comput. Prog. 51, 23–45 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Höfner, P., Möller, B., Solin, K. (2006). Omega Algebra, Demonic Refinement Algebra and Commands. In: Schmidt, R.A. (eds) Relations and Kleene Algebra in Computer Science. RelMiCS 2006. Lecture Notes in Computer Science, vol 4136. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11828563_15
Download citation
DOI: https://doi.org/10.1007/11828563_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37873-0
Online ISBN: 978-3-540-37874-7
eBook Packages: Computer ScienceComputer Science (R0)