Algebraic Derivation of Until Rules and Application to Timer Verification | SpringerLink
Skip to main content
Springer Nature Link
Log in

Algebraic Derivation of Until Rules and Application to Timer Verification

  • Conference paper
  • First Online:
Relational and Algebraic Methods in Computer Science (RAMiCS 2018)

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

  • 433 Accesses

Abstract

Using correspondences between linear temporal logic and modal Kleene Algebra, we prove in an algebraic manner rules of linear temporal logic involving the until operator. These can be used to verify programmable logic controllers; as a case study we use a part of the control of pedestrian lights, verified with the interactive tool KIV.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    This abstracts from the classical LTL semantics in terms of sets of infinite traces of program states. That concrete semantics is mirrored by a modal semiring in which the elements are relations between sets of traces and tests are sets of traces; states in the sense of the above wording are then single traces, not program states.

  2. 2.

    Note that this is not the same as , which does not hold.

References

  1. Coq. https://coq.inria.fr/. Accessed 7 July 2015

  2. IEC61131. http://webstore.iec.ch/webstore/webstore.nsf/artnum/048541!opendocument. Accessed 20 Mar 2018

  3. The KIV system. http://www.isse.uni-augsburg.de/en/software/kiv/. Accessed 20 Mar 2018

  4. NuSMVExamples. http://nusmv.fbk.eu/examples/examples.html. Accessed 7 Aug 2018

  5. Step7. http://w3.siemens.com/mcms/simatic-controller-software/en/step7/Pages/Default.aspx. Accessed 20 Mar 2018

  6. Verification of pedestrian lights in MKA. http://rolandglueck.de/Downloads/Pedestrian_lights_verified.zip. Accessed 20 Mar 2018

  7. VerifyThis 2015. http://verifythis2015.cost-ic0701.org/results. Accessed 8 Aug 2018

  8. VerifyThis 2017. http://www.pm.inf.ethz.ch/research/verifythis/Archive/2017.html. Accessed 8 Aug 2018

  9. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  10. Back, R.-J., von Wright, J.: Refinement Calculus - A Systematic Introduction. Graduate Texts in Computer Science. Springer, New York (1998)

    Book  Google Scholar 

  11. Ben-Ari, M.: Mathematical Logic for Computer Science, 3rd edn. Springer, London (2012)

    Book  Google Scholar 

  12. Berghammer, R., Stucke, I., Winter, M.: Using relation-algebraic means and tool support for investigating and computing bipartitions. J. Log. Algebr. Meth. Prog. 90, 102–124 (2017)

    Article  Google Scholar 

  13. Birkhoff, G.: Lattice Theory, 3rd edn. American Mathematical Society, Providence (1967)

    Google Scholar 

  14. Brunet, P., Pous, D., Stucke, I.: Cardinalities of finite relations in Coq. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 466–474. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-43144-4_29

    Chapter  Google Scholar 

  15. Carlsson, H., Svensson, B., Danielson, F., Lennartson, B.: Methods for reliable simulation-based PLC code verification. IEEE Trans. Ind. Inform. 8(2), 267–278 (2012)

    Article  Google Scholar 

  16. Desharnais, J., Möller, B.: Non-associative Kleene algebra and temporal logics. In: Höfner, P., Pous, D., Struth, G. (eds.) RAMICS 2017. LNCS, vol. 10226, pp. 93–108. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57418-9_6

    Chapter  MATH  Google Scholar 

  17. Desharnais, J., Möller, B., Struth, G.: Modal Kleene algebra and applications - a survey. J. Relat. Methods Comput. Sci. 1, 93–131 (2004)

    MATH  Google Scholar 

  18. Ehm, T., Möller, B., Struth, G.: Kleene modules. In: Berghammer, R., Möller, B., Struth, G. (eds.) RelMiCS 2003. LNCS, vol. 3051, pp. 112–123. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24771-5_10

    Chapter  MATH  Google Scholar 

  19. Ertel, J.: Verifikation von SPS-Programmen MIT Kleene Algebra. Master’s thesis, Institut of Informatics, University of Augsburg (2017)

    Google Scholar 

  20. Ésik, Z., Fahrenberg, U., Legay, A., Quaas, K.: Kleene algebras and semimodules for energy problems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 102–117. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02444-8_9

    Chapter  MATH  Google Scholar 

  21. Glück, R., Krebs, F.B.: Towards interactive verification of programmable logic controllers using modal Kleene algebra and KIV. In: Kahl, W., Winter, M., Oliveira, J.N. (eds.) RAMICS 2015. LNCS, vol. 9348, pp. 241–256. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24704-5_15

    Chapter  MATH  Google Scholar 

  22. Gondran, M., Minoux, M.: Graphs, Dioids and Semirings. Springer, Heidelberg (2008)

    MATH  Google Scholar 

  23. Guttmann, W.: Stone relation algebras. In: Höfner, P., Pous, D., Struth, G. (eds.) RAMICS 2017. LNCS, vol. 10226, pp. 127–143. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57418-9_8

    Chapter  Google Scholar 

  24. Höfner, P., Möller, B.: Dijkstra, Floyd and Warshall meet Kleene. Formal Asp. Comput. 24(4–6), 459–476 (2012)

    Article  MathSciNet  Google Scholar 

  25. Hollenberg, M.: An equational axiomatization of dynamic negation and relational composition. J. Log. Lang. Inf. 6(4), 381–401 (1997)

    Article  MathSciNet  Google Scholar 

  26. Hollenberg, M.: Equational axioms of test algebra. In: Nielsen, M., Thomas, W. (eds.) CSL 1997. LNCS, vol. 1414, pp. 295–310. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028021

    Chapter  Google Scholar 

  27. Jackson, M., McKenzie, R.: Interpreting graph colorability in finite semigroups. IJAC 16(1), 119–140 (2006)

    MathSciNet  MATH  Google Scholar 

  28. Jee, E., Yoo, J., Cha, S.D., Bae, D.-H.: A data flow-based structural testing technique for FBD programs. Inf. Softw. Technol. 51(7), 1131–1139 (2009)

    Article  Google Scholar 

  29. Jipsen, P., Rose, H.: Varieties of Lattices, 1st edn. Springer, Heidelberg (1992)

    Book  Google Scholar 

  30. Kahl, W.: Graph transformation with symbolic attributes via monadic coalgebra homomorphisms. ECEASST 71, 5.1–5.17 (2014)

    Google Scholar 

  31. Kawahara, Y., Furusawa, H.: An algebraic formalization of fuzzy relations. Fuzzy Sets Syst. 101(1), 125–135 (1999)

    Article  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  33. Kozen, D.: Kleene algebra with tests. ACM Trans. Prog. Lang. Syst. 19(3), 427–443 (1997)

    Article  Google Scholar 

  34. Kröger, F., Merz, S.: Temporal Logic and State Systems. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2008)

    Google Scholar 

  35. Li, J., Qeriqi, A., Steffen, M., Yu, I.C.: Automatic translation from FBD-PLC-programs to NuSMV for model checking safety-critical control systems. In: NIK 2016. Bibsys Open Journal Systems, Norway (2016)

    Google Scholar 

  36. Litak, T., Mikulás, S., Hidders, J.: Relational lattices. In: Höfner, P., Jipsen, P., Kahl, W., Müller, M.E. (eds.) RAMICS 2014. LNCS, vol. 8428, pp. 327–343. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06251-8_20

    Chapter  MATH  Google Scholar 

  37. Manes, E., Benson, D.: The inverse semigroup of a sum-ordered semiring. Semigroup Forum 31, 129–152 (1985)

    Article  MathSciNet  Google Scholar 

  38. Michels, G., Joosten, S., van der Woude, J., Joosten, S.: Ampersand. In: de Swart, H. (ed.) RAMICS 2011. LNCS, vol. 6663, pp. 280–293. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21070-9_21

    Chapter  MATH  Google Scholar 

  39. 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). https://doi.org/10.1007/11784180_21

    Chapter  MATH  Google Scholar 

  40. Möller, B., Roocks, P.: An algebra of database preferences. J. Log. Algebr. Meth. Program. 84(3), 456–481 (2015)

    Article  MathSciNet  Google Scholar 

  41. Oliveira, J.N.: A relation-algebraic approach to the “Hoare logic” of functional dependencies. J. Log. Algebr. Meth. Prog. 83(2), 249–262 (2014)

    Article  Google Scholar 

  42. Pavlovic, O., Ehrich, H.-D.: Model checking PLC software written in function block diagram. In: ICST 2010, CEUR Workshop Proceedings. IEEE Computer Society (2010)

    Google Scholar 

  43. Pratt, V.: Dynamic algebras: examples, constructions, applications. Studia Logica 50, 571–605 (1991)

    Article  MathSciNet  Google Scholar 

  44. Shannon, C.E.: Communication in the presence of noise. Proc. IRE 37(1), 10–21 (1949)

    Article  MathSciNet  Google Scholar 

  45. Solin, K., von Wright, J.: Enabledness and termination in refinement algebra. Sci. Comput. Prog. 74(8), 654–668 (2009)

    Article  MathSciNet  Google Scholar 

  46. von Karger, B.: Temporal algebra. Math. Struct. Comput. Sci. 8(3), 277–320 (1998)

    Article  MathSciNet  Google Scholar 

  47. Wan, H., Chen, G., Song, X., Gu, M.: Formalization and verification of PLC timers in Coq. In: Ahamed, S.I., et al. (eds.): Proceedings of the COMPSAC 2009, pp. 315–323. IEEE Computer Society (2009)

    Google Scholar 

  48. Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61–78. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_4

    Chapter  Google Scholar 

Download references

Acknowledgement

We are grateful to the anonymous referees for their careful scrutiny and helpful remarks.

Author information

Authors and Affiliations

  1. msg-life, Leinfelden-Echterdingen, Germany

    Jessica Ertel

  2. German Aerospace Center, Augsburg, Germany

    Roland Glück

  3. University of Augsburg, Augsburg, Germany

    Bernhard Möller

Authors
  1. Jessica Ertel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Roland Glück
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bernhard Möller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roland Glück .

Editor information

Editors and Affiliations

  1. Université Laval, Québec, QC, Canada

    Jules Desharnais

  2. University of Canterbury, Christchurch, New Zealand

    Walter Guttmann

  3. Open Universiteit, Heerlen, The Netherlands

    Stef Joosten

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ertel, J., Glück, R., Möller, B. (2018). Algebraic Derivation of Until Rules and Application to Timer Verification. In: Desharnais, J., Guttmann, W., Joosten, S. (eds) Relational and Algebraic Methods in Computer Science. RAMiCS 2018. Lecture Notes in Computer Science(), vol 11194. Springer, Cham. https://doi.org/10.1007/978-3-030-02149-8_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02149-8_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02148-1

  • Online ISBN: 978-3-030-02149-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics