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.
The third author would like to thank the EPSRC(UK), CNPq(Brasil), Imperial College, LMF-DI/PUC-RJ and The Royal Academy of
Engineering for their financial support during the conduct of this research.