Topos Semantics for a Higher-Order Temporal Logic of Actions
Logic in Computer Science
2020-09-16 v1
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.
Cite
@article{arxiv.2009.06834,
title = {Topos Semantics for a Higher-Order Temporal Logic of Actions},
author = {Philip Johnson-Freyd and Jon Aytac and Geoffrey Hulette},
journal= {arXiv preprint arXiv:2009.06834},
year = {2020}
}
Comments
In Proceedings ACT 2019, arXiv:2009.06334