Sam van Gool ; Adrien Guatto ; George Metcalfe ; Simon Santschi - Deciding Equations in the Time Warp Algebra

lmcs:10937 - Logical Methods in Computer Science, January 26, 2024, Volume 20, Issue 1 - https://doi.org/10.46298/lmcs-20(1:8)2024
Deciding Equations in the Time Warp AlgebraArticle

Authors: Sam van Gool ; Adrien Guatto ; George Metcalfe ; Simon Santschi

    Join-preserving maps on the discrete time scale $\omega^+$, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice -- called the time warp algebra -- that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover.


    Volume: Volume 20, Issue 1
    Published on: January 26, 2024
    Accepted on: December 20, 2023
    Submitted on: February 10, 2023
    Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic
    Funding:
      Source : OpenAIRE Graph
    • Modalities in Substructural Logics: Theory, Methods and Applications; Funder: European Commission; Code: 101007627
    • Proof and Order; Funder: Swiss National Science Foundation; Code: 165850

    Consultation statistics

    This page has been seen 785 times.
    This article's PDF has been downloaded 403 times.