Ertel, Jessica; Glück, Roland; Möller, Bernhard Algebraic derivation of until rules and application to timer verification. (English) Zbl 1518.68205 Desharnais, Jules (ed.) et al., Relational and algebraic methods in computer science. 17th international conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11194, 244-262 (2018). Summary: 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.For the entire collection see [Zbl 1398.68023]. Cited in 1 Document MSC: 68Q60 Specification and verification (program logics, model checking, etc.) 03B44 Temporal logic PDFBibTeX XMLCite \textit{J. Ertel} et al., Lect. Notes Comput. Sci. 11194, 244--262 (2018; Zbl 1518.68205) Full Text: DOI Link