论文标题
高阶时间逻辑的TOPOS语义
Topos Semantics for a Higher-Order Temporal Logic of Actions
论文作者
论文摘要
TLA是编写数字系统的口吃不变规范的流行时间逻辑。 但是，TLA缺乏高阶功能，可用于指定使用高阶编程语言编写的现代软件。 我们使用分类技术来根据一组时间膨胀或“斯托克”的作用来重塑TLA的实时语义，并通过纳入延迟或“步履蹒跚”的单体扩展。 通过将斯托特纳入步履蹒跚而引起的相关前topoi的几何形态，我们构建了高阶TLA的第一个模型。
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.
