计算机科学
时态逻辑
线性时序逻辑
区间时态逻辑
行动的时间逻辑
可判定性
计算树逻辑
理论计算机科学
动态逻辑(数字电子)
数学
线性逻辑
多模态逻辑
子结构逻辑
离散数学
程序设计语言
算法
自动机
扩展(谓词逻辑)
作者
Nan Zhang,Zhenhua Duan,Cong Tian
标识
DOI:10.1016/j.tcs.2021.02.007
摘要
Abstract This paper proposes a new temporal logic named Unified Temporal Logic (UTL). First, the syntax and semantics of UTL are inductively defined. Further, logic laws in UTL are formalized and proved. Moreover, the normal forms of UTL formulas are defined and proved. To illustrate how to describe properties with UTL, an example of an elevator control system is given. In general, UTL combines the characteristics of Linear Temporal Logic (LTL) and Propositional Projection Temporal Logic (PPTL). So properties involving the “until” construct in LTL and the “chop” construct in PPTL can easily be represented in UTL. In addition, both finite and infinite models (intervals) are supported. With UTL, we are able to specify and verify some practical properties which cannot easily be formalized in LTL and PPTL.
科研通智能强力驱动
Strongly Powered by AbleSci AI