We present a logic for real time systems specification which is an extension of first order dynamic logic by adding (a) arbitrary atomic actions rather than only assignments, (b) variables over actions which allow to specify systems partially, and (c) explicit time. The logic is algebraized using closure fork algebras and a representation theorem for this class is presented. This allows to define an equational (but infinitary) proof system for the algebraization.
CITATION STYLE
Baum, G. A., Frias, M. F., & Maibaum, T. S. E. (1998). A logic for real-time systems specification, its algebraic semantics, and equational calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1548, pp. 91–105). Springer Verlag. https://doi.org/10.1007/3-540-49253-4_9
Mendeley helps you to discover research relevant for your work.