×

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

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B44 Temporal logic
PDFBibTeX XMLCite
Full Text: DOI Link