Abstract

The paper presents a new logical specification language, called Propositional Stabilisation Theory , to capture the stabilisation behaviour of combinational input-output systems. PST is an intuitionistic propositional modal logic interpreted over sets of waveforms. The language is more economic than conventional specification formalisms such as timed Boolean functions, temporal logic, or predicate logic in that it separates function from time and only introduces as much syntax as is necessary to deal with stabilisation behaviour. It is a purely propositional system but has second-order expressiveness. One and the same Boolean function can be represented in various ways as a PST formula, giving rise to different timing models which associate different stabilisation delays with different parts of the functionality and adjust the granularity of the data-dependency of delays within wide margins. We show how several standard timing analyses can be characterised as algorithms computing correct and exact stabilisation bounds for particular PST timing models. Specifically, the existence of a PST specification style for static sensitization solves the open exactness problem for this type of analysis. By choosing other timing models we can characterise timing analyses for which no algorithms so far exist. Translations between different timing models are the semantic basis for combining timing analyses.This work puts forward an application of intuitionistic modal logic that exploits the model-theoretic strength of the constructive approach. It contrasts with the traditional point of view that focuses on the proof-theoretic aspects of intuitionistic logic