返回首页
联手形式化方法专业委员会：“线性时序逻辑”术语发布|CCF术语快线
本期发布术语热词：线性时序逻辑(Linear temporal logic)
线性时序逻辑(Linear temporal logic) 作者：田聪（西安电子科技大学），刘关俊（同济大学） InfoBox： 中文名：线性时序逻辑 外文名：Linear temporal logic 简称：LTL 学科：计算机科学技术 实质：一种能表达时间概念的时序逻辑，采用线性、离散且与自然数同构的时间结构，以路径（状态序列）作为命题的论断对象，其公式在路径上解释其真值。 基本简介： 线性时序逻辑(Linear temporal logic, 简称LTL)由阿米尔·伯努利在1977年提出[10]，它将时间轴定义为一个线性序列，用于表示模型的动态语义，应用时序运算符描述从一个给定的状态开始的某一条路径上的事件。在LTL中，可以对关于路径上未来某时刻的公式进行编码，例如，一个事件最终将为真，或一个事件将为真直到另一个事件变为真，等等。 语法：LTL公式的递归定义如下： φ::= true | a |φ1∧φ2| ¬φ| Xφ|φ1 Uφ2 其中a为原子命题。 其余的布尔连接符和时序算子均可以由以上的布尔连接符和时序算子导出，例如φ1∧φ2 ≡ ¬(¬φ1∨¬φ2)，Fφ≡ true Uφ。 语义：给定一个无终端状态的变迁系统TS = (S, Act, →, I, AP, L)和它的一个路径π=s0s1s2…，定义π(i)=si, πi=sisi+1si+2…, 则π与LTL公式的满足关系|=递归定义如下[3]： （1） π|=true; （2） π|=a当且仅当a∈L(π(0)); （3） π|=φ1∧φ2当且仅当π|=φ1且π|=φ2; （4） π|=¬φ当且仅当π|=φ不成立; （5）π|=Xφ当且仅当π1|=φ; （6） π|=φ1 Uφ2当且仅当存在自然数i满足πi|=φ2且对任意的自然数j<i满足π⊨φ1。 对于一个变迁系统TS, TS|=φ当且仅当TS中的每一个路径π满足π|=φ。 LTL模型检测： 模型检测[1,2]是一种验证有限状态系统是否满足规范（如系统正确性、安全性等）的形式化方法，而LTL是表达规范的一种逻辑语言。对于LTL模型检测[3,4]，其过程如下图[19]所示，为了验证一个系统（TS表示）是否满足其对应的规范（LTL表示），首先把该规范的否定转成为与之等价的Büchi自动机，然后把它与系统模型求交得到新的自动机，最后在新的自动机上检查其接收的语言是否为空。如果为空则系统满足该规范，如果非空则系统不满足该规范并给出反例。 LTL模型检测器： 一般来说，LTL模型检测器可以分为具体的（explicit）和符号化的（symbolic）两种类型。具体的模型检测器如SPIN[5]，需要完全构造出整个状态空间来验证LTL公式；符号化的模型检测器如CadenceSMV[6]和NuSMV[7]，使用OBDD[8,9]数据结构符号化地表示和分析模型以验证LTL公式。 应用领域： LTL自从上个世纪七十年代被引入计算机科学领域之后[10]，得到了很大的发展。现如今，LTL作为一种形式化的性质规范描述，广泛应用于程序验证与分析[11,12]、程序综合[15]、数据库[13,14]和人工智能[16,17,18]等领域。 未来展望 LTL在程序验证与综合中的应用已非常成功，但如何降低状态复杂度仍是研究的难点。根据LTL的语义结构，将其直接转化为等价的确定性无穷字自动机，可大幅降低状态复杂度，提高效率[20]，这意味着LTL在程序验证与综合中的应用潜力仍可不断挖掘。此外，随着神经网络的广泛应用，其可信性备受关注。LTL及其扩展可形式化描述网络行为与相关属性[21]，特别是输入和输出之间的关系，为神经网络的验证提供有力支撑。LTL在保障神经网络乃至智能系统的可信性方面具有广阔的发展前景。 参考文献 [1] Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic[C]//Workshop on Logic of Programs. Springer, Berlin, Heidelberg, 1981: 52-71. [2] Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR[C]//International Symposium on programming. Springer, Berlin, Heidelberg, 1982: 337-351. [3] Baier C, Katoen J P. Principles of model checking[M]. MIT press, 2008. [4] Vardi M Y, Wolper P. An automata-theoretic approach to automatic program verification[C]//Proceedings of the First Symposium on Logic in Computer Science. IEEE Computer Society, 1986: 322-331. [5] Holzmann G J. The model checker SPIN[J]. IEEE Transactions on software engineering, 1997, 23(5): 279-295. [6] McMillan K L. The SMV language[J]. Cadence Berkeley Labs, 1999: 1-49. [7] Cimatti A, Clarke E, Giunchiglia F, et al. NuSMV: a new symbolic model checker[J]. International Journal on Software Tools for Technology Transfer, 2000, 2(4): 410-425. [8] Bryant R E. Graph-based algorithms for boolean function manipulation[J]. Computers, IEEE Transactions on, 1986, 100(8): 677-691. [9] Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020 states and beyond[J]. Information and computation, 1992, 98(2): 142-170. [10] Pnueli A. The temporal logic of programs[C]//18th Annual Symposium on Foundations of Computer Science (sfcs 1977). IEEE, 1977: 46-57. [11] Deutsch A, Sui L, Vianu V. Specification and verification of data-driven web services[C]//Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems. 2004: 71-82. [12] Huang Y W, Yu F, Hang C, et al. Verifying web applications using bounded model checking[C]//International Conference on Dependable Systems and Networks, 2004. IEEE, 2004: 199-208. [13] Vardi M Y. Automata theory for database theoreticians[M]//Theoretical Studies in Computer Science. Academic Press, 1992: 153-180. [14] Gligoric M, Majumdar R. Model checking database applications[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer, Berlin, Heidelberg, 2013: 549-564. [15] Vardi M Y. An automata-theoretic approach to linear temporal logic[M]//Logics for concurrency. Springer, Berlin, Heidelberg, 1996: 238-266. [16] Bacchus F, Kabanza F. Using temporal logics to express search control knowledge for planning[J]. Artificial intelligence, 2000, 116(1-2): 123-191. [17] Camacho A, Bienvenu M, McIlraith S A. Towards a unified view of AI planning and reactive synthesis[C]//Proceedings of the International Conference on Automated Planning and Scheduling. 2019, 29: 58-67. [18] Aminof B, De Giacomo G, Murano A, et al. Planning under LTL environment specifications[C]//Proceedings of the International Conference on Automated Planning and Scheduling. 2019, 29: 31-39. [19] 李建文. 线性时态逻辑中若干基础问题的研究[D]. 华东师范大学, 2014. [20]Esparza J, Křetínský J, Sickert S. A unified translation of linear temporal logic to ω-automata[J]. Journal of the ACM (JACM), 2020, 67(6): 33:1-33:61. [21] Liu W W, Song F, Zhang T H R, Wang J. Verifying ReLU Neural Networks from a Model Checking Perspective. Journal of Computer Science and Technology, 2020, 35: 1365–1381. 作者介绍 术语工委及术语平台介绍： 计算机术语审定委员会(Committee on Terminology)主要职能为收集、翻译、释义、审定和推荐计算机新词，并在CCF平台上宣传推广。这对厘清学科体系，开展科学研究，并将科学和知识在全社会广泛传播，都具有十分重要的意义。 术语众包平台CCFpedia的建设和持续优化，可以有效推进中国计算机术语的收集、审定、规范和传播工作，同时又能起到各领域规范化标准定制的推广作用。 新版的CCFpedia计算机术语平台(http://term.ccf.org.cn)将术语的编辑运营与浏览使用进行了整合，摒弃老版中跨平台操作的繁琐步骤，在界面可观性上进行了升级，让用户能够简单方便地查阅术语信息。同时，新版平台中引入知识图谱的方式对所有术语数据进行组织，通过图谱多层关联的形式升级了术语浏览的应用形态。 计算机术语审定工作委员会 主任： 刘挺（哈尔滨工业大学） 副主任： 王昊奋（同济大学） 李国良（清华大学） 主任助理： 李一斌（上海海乂知信息科技有限公司） 执行委员： 丁军（上海海乂知信息科技有限公司） 林俊宇（中国科学院信息工程研究所） 兰艳艳（清华大学） 张伟男（哈尔滨工业大学）
京公网安备 11010802032778号