Topos Semantics for a Higher-order Temporal Logic of Actions

被引：0
|
作者：
Johnson-Freyd, Philip [1 ]
Aytac, Jon [1 ]
Hulette, Geoffrey [1 ]
机构：
[1] Sandia Natl Labs, Albuquerque, NM 87123 USA
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2020年 / 323期
关键词：
D O I：
10.4204/EPTCS.323.11
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
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. (1)
引用
收藏
页码：161 / 171
页数：11
相关论文
共 50 条
  • [31] Higher-Order Coalition Logic
    Boella, Guido
    Gabbay, Dov M.
    Genovese, Valerio
    van der Torre, Leendert
    ECAI 2010 - 19TH EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2010, 215 : 555 - 560
  • [32] A logic of higher-order preferences
    Jiang, Junli
    Naumov, Pavel
    SYNTHESE, 2024, 203 (06)
  • [33] Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
    Charalambidis, Angelos
    Rondogiannis, Panos
    Symeonidou, Ioanna
    THEORY AND PRACTICE OF LOGIC PROGRAMMING, 2018, 18 (3-4) : 421 - 437
  • [34] Equivalence of two Fixed-Point Semantics for Definitional Higher-Order Logic Programs
    Charalambidis, Angelos
    Rondogiannis, Panos
    Symeonidou, Ioanna
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (191): : 18 - 32
  • [35] Equivalence of two fixed-point semantics for definitional higher-order logic programs
    Charalambidis, Angelos
    Rondogiannis, Panos
    Symeonidou, Ioanna
    THEORETICAL COMPUTER SCIENCE, 2017, 668 : 27 - 42
  • [36] Kripke semantics for higher-order type theory applied to constraint logic programming languages
    Lipton, James
    Nieva, Susana
    THEORETICAL COMPUTER SCIENCE, 2018, 712 : 1 - 37
  • [37] Temporal Higher-Order Contracts
    Disney, Tim
    Flanagan, Cormac
    McCarthy, Jay
    ACM SIGPLAN NOTICES, 2011, 46 (09) : 176 - 188
  • [38] Temporal Higher-Order Contracts
    Disney, Tim
    Flanagan, Cormac
    McCarthy, Jay
    ICFP 11 - PROCEEDINGS OF THE 2011 ACM SIGPLAN: INTERNATIONAL CONFERENCE ON FUNCTIONAL PROGRAMMING, 2011, : 176 - 188
  • [39] On the Relationship between Higher-Order Recursion Schemes and Higher-Order Fixpoint Logic
    Kobayashi, Naoki
    Lozes, Etienne
    Bruse, Florian
    ACM SIGPLAN NOTICES, 2017, 52 (01) : 246 - 259
  • [40] A real-time semantics of temporal logic of actions
    Kaminski, M
    Yariv, Y
    JOURNAL OF LOGIC AND COMPUTATION, 2003, 13 (06) : 921 - 937
12345