An Algebraic System of Temporal Structures

Lauchli and Leonard, in 1966, described a series of operations which are able to build all linear temporal structures up to first order equivalence. More recently these operations have been used to describe executions of continuous systems for the purposes of model checking real-time specifications. In this paper we present an algebra over these operations and show that it is both sound and complete, in that it can generate all equivalences over these models.