Parametric equations for temporal style assertions
Victor Yodaiken
TL;DR
The paper addresses how to specify temporal properties of reactive systems without full temporal logic by using sequential functions that map finite event sequences to outputs and by defining temporal-style operators on boolean-valued functions over these sequences. It develops a compositional, parametric-state framework with building blocks such as stores, toggles, and queues, and demonstrates real-time extensions via clocks and elapsed time to express timing and liveness properties, including a timing-enhanced Abadi–Lamport queue. Key contributions include formal definitions of Always, Eventually, Next, and Until over sequential functions, a detailed mechanism for composing components through connectors, and a correctness argument showing that timing constraints can enforce data integrity and order (e.g., $Q_O(w)$ is a prefix of $Q_I(w)$ under $Tspec$). The approach offers a practical, math-based alternative to temporal logic for OS and real-time system design, enabling precise reasoning about concurrency, timing, and composition via Moore-machine–style state evolution and sequential-function recursion.
Abstract
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.