Abstract
We introduce new variants of Kleene star and omega iteration for the case where the iterated operator is neither associative nor has a neutral element. The associated repetition algebras are used to give closed semantic expressions for the Until and While operators of the temporal logic \(\mathsf {CTL}^*\) and its sublogics \(\mathsf {CTL}\) and \(\mathsf {LTL}\). Moreover, the relation between the semantics of these logics can be expressed by homomorphisms between repetition algebras, which is a more systematic and compact approach than the ones taken in earlier papers.
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
Similar content being viewed by others
Notes
- 1.
In the literature this set is usually called \(\varSigma \). We avoid this, since throughout the paper we use \(\varSigma \) for sets of states.
- 2.
In the literature these are mostly called path formulas.
- 3.
We would have preferred the term iteration algebra which, however, is already used in [1] and follow-up papers with a different meaning.
- 4.
The subscript \(_d\) stands for “domain”.
References
Bloom, S., Ésik, Z.: Iteration algebras. Int. J. Found. Comput. Sci. 3(3), 245–302 (1992)
Conway, J.: Regular Algebra and Finite Machines. Chapman & Hall, Boca Raton (1971)
Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebras. Inf. Sci. 139, 253–273 (2001)
Desharnais, J., Möller, B.: Non-associative Kleene algebra and temporal logics. https://www.informatik.uni-augsburg.de/de/lehrstuehle/dbis/pmi/publications/all_pmi_tech-reports/tr-RAMICS16/
Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Logic 7, 798–833 (2006)
Dijkstra, R.M.: Computation calculus bridging a formalisation gap. Sci. Comput. Program. 37, 3–36 (2000)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Vol. B: Formal Models and Semantics, pp. 995–1072. Elsevier, Amsterdam (1991)
Kleene, S.: Representation of events in nerve nets and finite automata. In: Shannon, C., McCarthy, J. (eds.) Automata Studies, pp. 3–41. Princeton University Press, Princeton (1956)
Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)
Kozen, D.: Kleene algebras with tests. ACM Trans. Program. Lang. Syst. 19, 427–443 (1997)
Kozen, D.: Some results in dynamic model theory. Sci. Comput. Program. 51, 3–22 (2004)
Möller, B.: Lazy Kleene algebra. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 252–273. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27764-4_14. Revised version in [13]
Möller, B.: Kleene getting lazy. Sci. Comput. Program. 65, 195–214 (2007)
Möller, B., Hoare, T.: Exploring an interface model for CKA. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 1–29. Springer, Cham (2015). doi:10.1007/978-3-319-19797-5_1
Möller, B., Höfner, P., Struth, G.: Quantales and temporal logics. In: Johnson, M., Vene, V. (eds.) AMAST 2006. LNCS, vol. 4019, pp. 263–277. Springer, Heidelberg (2006). doi:10.1007/11784180_21
Rosenthal, K.: Quantales and their applications. Pitman Research Notes in Math. No. 234 Longman Scientific and Technical (1990)
Schmidt, G., Ströhlein, T.: Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)
Acknowledgement
We are grateful to Roland Glück and to the anonymous referees for valuable comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Desharnais, J., Möller, B. (2017). Non-associative Kleene Algebra and Temporal Logics. In: Höfner, P., Pous, D., Struth, G. (eds) Relational and Algebraic Methods in Computer Science. RAMICS 2017. Lecture Notes in Computer Science(), vol 10226. Springer, Cham. https://doi.org/10.1007/978-3-319-57418-9_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-57418-9_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-57417-2
Online ISBN: 978-3-319-57418-9
eBook Packages: Computer ScienceComputer Science (R0)