Topos Semantics for a Higher-Order Temporal Logic of Actions

TL;DR

This paper introduces a higher-order extension of TLA, a temporal logic, using categorical methods to model real-time semantics with actions representing time dilations and delays.

Contribution

It develops the first model of higher-order TLA by employing categorical techniques and presheaf topoi to incorporate higher-order features into the logic.

Findings

Categorical techniques successfully model real-time semantics for TLA.

Construction of the first higher-order TLA model.

Use of geometric morphisms to relate stutters and falters.

Abstract

TLA is a popular temporal logic for writing stuttering-invariant specifications of digital systems. However, TLA lacks higher-order features useful for specifying modern software written in higher-order programming languages. We use categorical techniques to recast a real-time semantics for TLA in terms of the actions of a group of time dilations, or "stutters," and an extension by a monoid incorporating delays, or "falters." Via the geometric morphism of the associated presheaf topoi induced by the inclusion of stutters into falters, we construct the first model of a higher-order TLA.