<commit_before>---
layout: post
title:  正文
---

线性时态逻辑可满足性工具的设计与实现
=========

##第一章 绪论

###1.1 线性时态逻辑的发展

时态逻辑，简而言之，就是研究包含时态词“过去”、“现在”、“将来”等等的命题及其推理的科学。
其历史最早可追溯至古希腊的麦加拉派，此后亚里士多德、阿维森那、中世纪经院学者都对此作过片断论述。
而直到20世纪，这个概念才由英国逻辑学家<NAME>首先提出，其书《时间与模态》（Time and Modality）[1]给出了第一个时态逻辑的系统。

此后时态逻辑得到了很大的发展，并于1977年首次被引入计算机科学领域[2]，此人便是<NAME>，他将其作为形式化的规范语言引入到程序验证与分析领域。
在Pnueli的书中，提出了“将来线性时态逻辑”，也就是本文所讨论的线性时态逻辑（LTL），我们将在接下去的第二章中介绍该语法语义。

然而，线性时态逻辑能被广泛应用的一个理论基础便是其表达能力等价于一阶谓词逻辑[3]（而在可满足性、可判定性等问题上的难易程度却天差地别）。
既然线性时态逻辑的表达能力等价于一阶谓词逻辑，而自动机理论又告诉我们一阶谓词逻辑可以转为自动机，那么我们可以有以下推论：
线性时态逻辑可以用自动机来表示，至少可以通过先将线性时态逻辑转为一阶谓词逻辑，再将一阶谓词逻辑转为自动机来实现，
但事实是，此过程的复杂度是不可承受的。
1983年，Wolper等人发现其转化过程并不需要如此复杂，提出了一个PSPACE-完全的上界[4]。

终于，关于线性时态逻辑最基本的理论框架搭建完成。
现如今，线性时态逻辑作为一种形式化的性质规范描述，已在程序验证与分析、程序综合、数据库和人工智能等领域被广泛使用。

###1.2 线性时态逻辑的应用场景


<br />
<br />
<br />
<br />
<br />

[1] A. Prior. Time and Modality. Oxford University Press, 1957.

[2] <NAME>. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foun- dations of Computer Science, pages 46–57, 1977.

[3] <NAME>, <NAME>, <NAME>, and <NAME>. On the temporal analysis of fairness. In Proc. 7th ACM Symp. on Principles of Programming Languages, pages 163– 173, 1980.

[4] <NAME> and <NAME>. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.<commit_msg>完成第二章第一节<commit_after>---
layout: post
title:  正文
---

线性时态逻辑可满足性工具的设计与实现
=========

##第一章 绪论

###1.1 线性时态逻辑的发展

时态逻辑，简而言之，就是研究包含时态词“过去”、“现在”、“将来”等等的命题及其推理的科学。
其历史最早可追溯至古希腊的麦加拉派，此后亚里士多德、阿维森那、中世纪经院学者都对此作过片断论述。
而直到20世纪，这个概念才由英国逻辑学家Arthur Norman Prior首先提出，其书《时间与模态》（Time and Modality）[1]给出了第一个时态逻辑的系统。

此后时态逻辑得到了很大的发展，并于1977年首次被引入计算机科学领域[2]，此人便是<NAME>，他将其作为形式化的规范语言引入到程序验证与分析领域。
在Pnueli的书中，提出了“将来线性时态逻辑”，也就是本文所讨论的线性时态逻辑（LTL），我们将在接下去的第二章中介绍该语法语义。

然而，线性时态逻辑能被广泛应用的一个理论基础便是其表达能力等价于一阶谓词逻辑[3]（而在可满足性、可判定性等问题上的难易程度却天差地别）。
既然线性时态逻辑的表达能力等价于一阶谓词逻辑，而自动机理论又告诉我们一阶谓词逻辑可以转为自动机，那么我们可以有以下推论：
线性时态逻辑可以用自动机来表示，至少可以通过先将线性时态逻辑转为一阶谓词逻辑，再将一阶谓词逻辑转为自动机来实现，
但事实是，此过程的复杂度是不可承受的。
1983年，Wolper等人发现其转化过程并不需要如此复杂，提出了一个PSPACE-完全的上界[4]。

终于，关于线性时态逻辑最基本的理论框架搭建完成。
现如今，线性时态逻辑作为一种形式化的性质规范描述，已在程序验证与分析、程序综合、数据库和人工智能等领域被广泛使用。

(...)
<!-- ###1.2 LTL可满足性 -->


##第二章 算法描述

###2.1 基础概念

我们令AP为一个原子的集合，那么线性时态逻辑的公式φ的语法可以定义为：

```
φ ::= true| false| a| ¬φ| φ1∧φ2| φ1∨φ2| Xφ| φ1Uφ2| φ1Rφ2| Gφ| Fφ
```

其中，a ∈ AP，¬、∧和∨为命题逻辑算子，X(next)、U(until)、R(release)、G(global)和F(future)为时态逻辑算子。

以下我们解释一下各时态逻辑算子：

* Xφ 表示下一个状态φ要成立
* φ1Uφ2 表示存在某一个状态使得φ2成立,并且这之前φ1都成立
* φ1Rφ2 ::= ¬(¬φ1U ¬φ2)
* Gφ ::= false R φ
* Fφ ::= true U φ

由上述定义可知，命题逻辑公式可以理解为是一种不包含时态算子的LTL公式。
这里，我们引入否定范式的概念，即将所有的否定符号只放在原子之前的公式，在李建文博士的博士论文中向我们证明：
任意一个LTL公式φ都有一个否定范式与它等价[5]。




<br />
<br />
<br />
<br />
<br />

[1] A. Prior. Time and Modality. Oxford University Press, 1957.

[2] <NAME>. The temporal logic of programs. In Proc. 18th IEEE Symp. on Foun- dations of Computer Science, pages 46–57, 1977.

[3] <NAME>, <NAME>, <NAME>, and <NAME>. On the temporal analysis of fairness. In Proc. 7th ACM Symp. on Principles of Programming Languages, pages 163– 173, 1980.

[4] <NAME> and <NAME>. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 1994.

[5] 李建文. 线性时态逻辑中若干基础问题的研究. 2014
{'fraction_non_alphanumeric': 0.14002557544757033, 'fraction_numerical': 0.04475703324808184, 'mean_word_length': 7.023076923076923, 'pattern_counts': {'":': 0, '<': 31, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4709344', 'n_tokens_mistral': 2343, 'n_tokens_neox': 2674, 'n_words': 246}