Parametric equations for temporal style assertions

Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by making referencing the state graph implicitly. This paper shows how to get the same effect, with a finer control over specification and a compositional notion of state, using ordinary working mathematics, without the weight of formal logic, by using parametric state variables.