Theorem Proving for Metric Temporal Logic over the Naturals

被引：5
|
作者：
Hustadt, Ullrich [1 ]
Ozaki, Ana [2 ]
Dixon, Clare [1 ]
机构：
[1] Univ Liverpool, Dept Comp Sci, Liverpool, Merseyside, England
[2] Tech Univ Dresden, Ctr Adv Elect Dresden Cfaed, Dresden, Germany
来源：
AUTOMATED DEDUCTION - CADE 26 | 2017年 / 10395卷
关键词：
PUNCTUALITY; COMPLEXITY;
D O I：
10.1007/978-3-319-63046-5_20
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We study translations from Metric Temporal Logic (MTL) over the natural numbers to Linear Temporal Logic (LTL). In particular, we present two approaches for translating from MTL to LTL which preserve the ExpSpace complexity of the satisfiability problem for MTL. In each of these approaches we consider the case where the mapping between states and time points is given by (1) a strict monotonic function and by (2) a non-strict monotonic function (which allows multiple states to be mapped to the same time point). Our translations allow us to utilise LTL solvers to solve satisfiability and we empirically compare the translations, showing in which cases one performs better than the other.
引用
收藏
页码：326 / 343
页数：18
相关论文
共 50 条
  • [1] Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
    Hustadt, Ullrich
    Ozaki, Ana
    Dixon, Clare
    [J]. JOURNAL OF AUTOMATED REASONING, 2020, 64 (08) : 1553 - 1610
  • [2] Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
    Hustadt, Ullrich
    Ozaki, Ana
    Dixon, Clare
    [J]. Journal of Automated Reasoning, 2020, 64 (08): : 1553 - 1610
  • [3] Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
    Ullrich Hustadt
    Ana Ozaki
    Clare Dixon
    [J]. Journal of Automated Reasoning, 2020, 64 : 1553 - 1610
  • [4] Interactive Theorem Proving with Temporal Logic
    Felty, A.
    Thery, L.
    [J]. Journal of Symbolic Computation, 23 (04):
  • [5] Interactive theorem proving with temporal logic
    Felty, A
    Thery, L
    [J]. JOURNAL OF SYMBOLIC COMPUTATION, 1997, 23 (04) : 367 - 397
  • [6] Automated Theorem Proving in Temporal Logic:T-Resolution
    招兆铿
    戴军
    陈文丹
    [J]. Journal of Computer Science & Technology, 1994, (01) : 53 - 62
  • [7] Question answering over logic puzzles using theorem proving
    Groza, Adrian
    Nitu, Cristian
    [J]. 37TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, 2022, : 871 - 874
  • [8] Theorem proving for intensional logic
    [J]. 1600, Kluwer Academic Publishers, Dordrecht, Netherlands (14):
  • [9] Automated theorem proving in temporal logic. T-resolution
    Zhaokeng, Zhao
    Jun, Dai
    Wendan, Chen
    [J]. Journal of Computer Science and Technology, 1994, 9 (01)
  • [10] Proving linearizability with temporal logic
    Baeumler, Simon
    Schellhorn, Gerhard
    Tofan, Bogdan
    Reif, Wolfgang
    [J]. FORMAL ASPECTS OF COMPUTING, 2011, 23 (01) : 91 - 112
12345