Parametric equations for temporal style assertions

TL;DR

This paper introduces a method to specify temporal properties in reactive software using sequential functions, offering finer control and compositionality without relying on traditional temporal logic.

Contribution

It presents an alternative to temporal logic for specifying temporal assertions using sequential functions, simplifying the approach and enhancing control.

Findings

Sequential functions can effectively represent temporal assertions.

The method provides finer control over specifications.

It offers a compositional notion of state.

Abstract

Temporal logic provided an appealing approach to specifying properties of operating systems and other "reactive" software by allowing propositions to be qualified by "when" they must be true. 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 sequential functions which are an alternate representation of Moore type state machines.