释义：Linear temporal logic （LTL）浅析

文章目录

前言
正文
小结
参考文献

前言

创作开始时间：2021年3月22日07:55:11

如题。简要解释一下LTL线性时间逻辑。

正文

主要参考：

wiki词条：Linear_temporal_logic

LTL，全称为：linear temporal logic，也叫linear-time temporal logic。

Wiki解释：

In logic, linear temporal logic or linear-time temporal logic[1][2] (LTL) is a modal temporal logic with modalities referring to time

在逻辑中，线性时间逻辑，或者线性时间时序逻辑是一个模态时序逻辑，其模态指的是时间。

In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. Subsequently, LTL is sometimes called propositional temporal logic, abbreviated PTL.[3] In terms of expressive power, linear temporal logic (LTL) is a fragment of first-order logic.[4][5]

LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.[6]

在LTL中，我们可以将公式编码成未来路径。如：一个条件最终为真等。LTL是一阶逻辑。

LTL最早被Amir Pnueli在1977年提出，用来做计算机程序的形式化检验。

（然后就是一串公式，此处不详述。大概了解即可。）

小结

有关LTL的详细解释可以进一步参考：

Linear Temporal Logic
Temporal Logic

我只是想简单了解下，所以到此暂止。

创作结束时间：2021年3月22日08:05:47

参考文献

wiki词条：Linear_temporal_logic

释义：Linear temporal logic （LTL）浅析相关推荐

【论文随笔】Transfer of temporal logic formulas in reinforcement learning
Zhe Xu and Ufuk Topcu. 2019. Transfer of temporal logic formulas in reinforcement learning. In Proce ...
【释义】NP complete概念浅析（涵盖：P问题，NP问题，NP完全问题，NP难问题）
文章目录前言正文 1.P问题 2.NP问题 3.NP-complete问题(即:NP完全问题) 4.NP完全问题可能不会长久存在 5.示例 6.NP-Hard问题(即:NP难问题) 7.关系小结 ...
线性时态逻辑ctl_基于决策过程的广义可能性时态逻辑模型检测
基于决策过程的广义可能性时态逻辑模型检测 [摘要]:随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性,已成为大家广泛探讨的问题.模型检测由于其借助严格的数学方法来验证系统是否满足性质和自动化验证 ...
系统分析与验证课程笔记——目录
目录参考资料与引用目录前置知识知识图谱后记这个系列是研究生"系统分析与验证课程"的课程笔记记录,因为有好多篇,为了方便索引,所以写了这篇目录,也是为了能让有需要的人能够 ...
八卦一下模型验证（一） (转自g9老大的八卦系列）
好遗憾,直到最近才无意间在CSDN发现这么牛逼的一坨博客.我一直以为MC只是学术界的事情,工业界哪可能会有人静下心来研究这个呢?看完之后真是激动万分啊,这是一个很棒的科普系列文章.也正是我在做的课题. ...
写给学生看的系统分析与验证笔记（十五）——计算树逻辑(Computation tree logic,CTL)
目录介绍计算树线性时间和分支时间的对比 CTL的语法 CTL的语义 CTL状态公式的语义 CTL路径公式的语义 CTL在TS上的语义 CTL等价的定义 CTL公式的性质介绍在前面我们已经介绍 ...
形式化语言——时序逻辑
时序逻辑在模型检测工具NuSMV中,时序逻辑是用来描述系统性质(或形式规约)的形式化语言,包括两类,一类是线性时序逻辑(Linear-time Temporal Logic, LTL),另一类是分 ...
模型检测原理、方法学习
模型检测学习一.模型检测概论 1.1 模型检测所解决的问题:保证并发系统正确性和可靠性 1.2 特点:自动化程度高.简洁明了 1.3 发展:用于描述并发系统性质的CTL逻辑符号模型检测技术 1.4 ...
计算机专业英语词汇缩写大全(J-Z)
转载自:http://hi.baidu.com/zhanglianzhang/blog/item/3fb22dd30f68f30b3af3cfbd.html J J2EE - Java 2 Enter ...

释义：Linear temporal logic （LTL）浅析

文章目录

前言

正文

小结

参考文献

释义：Linear temporal logic （LTL）浅析相关推荐

最新文章

热门文章