Skip to main content
SpringerLink
Log in

Non-associative Kleene Algebra and Temporal Logics

  • Conference paper
  • First Online:
Relational and Algebraic Methods in Computer Science (RAMICS 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10226))

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

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 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. 2.

    In the literature these are mostly called path formulas.

  3. 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. 4.

    The subscript \(_d\) stands for “domain”.

References

  1. Bloom, S., Ésik, Z.: Iteration algebras. Int. J. Found. Comput. Sci. 3(3), 245–302 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  2. Conway, J.: Regular Algebra and Finite Machines. Chapman & Hall, Boca Raton (1971)

    MATH  Google Scholar 

  3. Desharnais, J., Möller, B.: Characterizing determinacy in Kleene algebras. Inf. Sci. 139, 253–273 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  4. 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/

  5. Desharnais, J., Möller, B., Struth, G.: Kleene algebra with domain. ACM Trans. Comput. Logic 7, 798–833 (2006)

    Article  MathSciNet  Google Scholar 

  6. Dijkstra, R.M.: Computation calculus bridging a formalisation gap. Sci. Comput. Program. 37, 3–36 (2000)

    Article  MATH  Google Scholar 

  7. 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)

    Google Scholar 

  8. 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)

    Google Scholar 

  9. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Inf. Comput. 110, 366–390 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  10. Kozen, D.: Kleene algebras with tests. ACM Trans. Program. Lang. Syst. 19, 427–443 (1997)

    Article  Google Scholar 

  11. Kozen, D.: Some results in dynamic model theory. Sci. Comput. Program. 51, 3–22 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  12. 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]

    Chapter  Google Scholar 

  13. Möller, B.: Kleene getting lazy. Sci. Comput. Program. 65, 195–214 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  14. 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

    Chapter  Google Scholar 

  15. 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

    Chapter  Google Scholar 

  16. Rosenthal, K.: Quantales and their applications. Pitman Research Notes in Math. No. 234 Longman Scientific and Technical (1990)

    Google Scholar 

  17. Schmidt, G., Ströhlein, T.: Relations and Graphs: Discrete Mathematics for Computer Scientists. EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg (1993)

    Book  MATH  Google Scholar 

Download references

Acknowledgement

We are grateful to Roland Glück and to the anonymous referees for valuable comments.

Author information

Authors and Affiliations

  1. Université Laval, Quebec City, QC, Canada

    Jules Desharnais

  2. Institut für Informatik, Universität Augsburg, Augsburg, Germany

    Bernhard Möller

Authors
  1. Jules Desharnais
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bernhard Möller .

Editor information

Editors and Affiliations

  1. Data61, CSIRO, Sydney, New South Wales, Australia

    Peter Höfner

  2. CNRS, Lyon, France

    Damien Pous

  3. University of Sheffield, Sheffield, United Kingdom

    Georg Struth

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation