计算机数理逻辑-时序逻辑-语法与语义

1. Introduction

Temporal logic is a formal system for reasoning about time. Temporal logic has found extensive application in computer science, because the behavior of both hardware and software is a function of time.

Temporal logics are related to formal systems called modal logics. Modal logics express the distinction between what is necessarily true and what is possibly true. For example, the statement ‘7 is a prime number’ is necessarily true because—given the definitions of the concepts in the statement—the statement is true always and everywhere. In contrast, the statement the head of state of this country is a king is possibly true, because its truth changes from place to place and from time to time. Temporal logic and modal logic are related because ‘always’ is similar to ‘necessarily’ and ‘eventually’ to ‘possibly’.

时间逻辑与称为模态逻辑的形式系统有关。模态逻辑表达了什么是必然真实和什么是可能真实之间的区别。例如，”7是质数 “这个陈述必然是真实的，因为–考虑到陈述中概念的定义–这个陈述总是真实的，而且无处不在。相比之下，这个国家的国家元首是国王的说法可能是真的，因为它的真理在不同的地方和不同的时间会发生变化。时间逻辑和模态逻辑是相关的，因为 “总是 “类似于 “必然”，”最终 “类似于 “可能”。

• 时间逻辑与模态逻辑相似，只是状态被认为是指定在某一特定时间点上的真实情况，而转换则定义了时间的流逝

2. PTL

2.1. Syntax

• The syntax of propositional temporal logic (PTL) is defined like the syntax of propositional logic, except for the addition of two additional unary operators:
  • □ , read always
  • ◊ , read eventually
• $(¬ ◊p)∧(□¬ q)$
  • the temporal operators and negation have higher precedence优先权 than the conjunction operator

2.2. semantic

• Informally, □ is a universal operator meaning ‘for any time t in the future’, while ◊ is an existential operator meaning ‘for some time t in the future’

2.3. transition diagram 状态转换图

• Interpretations of PTL formulas are based upon state transition diagrams.

  • The intuitive直观 meaning is that each state represents a world and a formula can have different truth values in different worlds. The transitions represent changes from one world to another.

• A state transition diagram is a directed graph有向图.

  • The nodes are states and the edges are transitions. 节点是状态，边是转换
  • Each state is labeled with a set of propositional literals such that clashing literals do not appear in any state. 每个状态都标有一个命题字面量的集合，这样冲突的字面量就不会出现在任何状态中

• A formula that contains a temporal operator is interpreted using the transitions between the states

  • 一个包含时间运算符的公式被解释为使用状态之间的转换

• If an atom is not shown in the label of a state, it is assumed to be assigned F.

• $s:P \rightarrow { T,F }$
• A binary relation can be considered to be a mapping from a state to a set of states $ρ:S→2^{S}$ , so the relational notation $(s_1,s_2)∈ρ$ will usually be written functionally as $s_2∈ρ(s_1)$
  • 注意$s_1$和$s_2$顺序关系

2.4. truth value

• 注意最后一行得notation

• $ρ(s_0)={s_1,s_2}$. Since $s_1⊨q$ and $s_2⊨q$, it follows that $s_0⊨□q$. By the semantics of $∨$, $s _0⊨□p∨□q$.

• $s_3∈ρ(s_1)$, but $s_3 \not\models p$ and $s_3 \not\models q$ , so $s_1 \not\models □p$ and $s_1 \not\models □q$ . Therefore, $s_1 \not\models □p \lor □q$

2.5. Satisfiability and Validity

The definition of semantic properties in PTL is more complex than it is in propositional or first-order logic, because an interpretation consists of both states and truth values

There are other formulas of PTL that are valid because of properties of temporal logic and not as instances of propositional validities. We will prove the validity of two formulas directly from the semantic definition. The first establishes a duality between □ and ◊, and the second is the distribution of □ over →, similar to the distribution of ∀ over →.

2.5.1. Duality

• $⊨□p↔¬ ◊¬ p$

3. Models of Time

In modal and temporal logics, different logics can be obtained by placing restrictions on the transition relation

• 在模态和时间逻辑中，通过对转换关系的限制可以得到不同的逻辑

• 也就是说True value无关，逻辑是通过transition relation实现的

3.1. Reflexivity

• An interpretation $I=(S,ρ)$ is reflexive iff $ρ$ is a reflexive relation: for all $s \in S$, $(s,s)∈ρ$, or $s∈ρ(s)$ in functional notation.
  • 放在状态图上就是个自己指向自己的圈

3.2. Transitivity

• An interpretation with a transitive relation is characterized by the formula $□A→□□A$ (or by the formula $◊◊A→◊A$)
• In an interpretation that both is reflexive and transitive, $⊨□A↔□□A$ and $⊨◊A↔◊◊A$.

3.3. Linearity 线性关系

• An interpretation $I=(S,ρ)$ is linear if $ρ$ is a function, that is, for all $s \in S$, there is at most one $s^{‘} \in S$ such that $s^{‘} ∈ρ(s)$
  • 也就是最少没有后续状态，最多一个后续状态

It might appear that a linear temporal logic would be limited to expressing properties of sequential programs and could not express properties of concurrent programs, where each state can have several possible successors depending on the interleaving of the statements of the processes. However, linear temporal logic is successful precisely in the context of concurrent programs because there is an implicit universal quantification in the definitions

看起来线性时态逻辑仅限于表达顺序程序的属性，而不能表达并发程序的属性，因为在并发程序中，每个状态可以有几个可能的后继者，这取决于进程语句的交错情况。然而，线性时间逻辑恰恰在并发程序的背景下是成功的，因为在定义中有一个隐含的普遍量化

example

• a temporal logic formula like $A=□◊running$
• In any state, the execution will eventually reach a state in which the computation is running
• The program will be correct if this formula is true in every possible execution of the program obtained by interleaving the instructions of its processes.
  • Each interleaving交错 can be considered as a single linear interpretation, so if we prove $\models{_I} A$ for an arbitrary linear interpretation $I$, then the correctness property holds for the program

3.4. Discreteness 离散

Although the passage of time is often considered to be continuous and expressible by real numbers, the execution of a program is considered to be a sequence of discrete steps, where each step consists of the execution of a single instruction of the CPU. Thus it makes sense to express the concept of the next instant in time. To express discrete steps in temporal logic, an additional operator is added

• 虽然时间的流逝通常被认为是连续的，可以用实数来表达，但程序的执行被认为是一连串离散的步骤，其中每一步都包括执行CPU的一条指令。因此，用时间来表达下一个瞬间的概念是有意义的。为了在时间逻辑中表达离散的步骤，我们增加了一个额外的操作符

• The unary operator $\bigcirc$ is called next
• truth value
  • f $A$ is $\bigcirc A^{‘}$ then $v(A)=T$ iff $v(A^{‘})=T$ for some $s^{‘}∈ρ(s)$
  • 显然后面的状态想要是T那么前面的状态肯定得是T，但只需要some就行
• 注意要$\bigcirc A$为T，只需A指向的state为T，和$A$本身T或F没有关系

3.4.1. self-dual

• $\bigcirc A \leftrightarrow \lnot \bigcirc \lnot A$

The operator $\bigcirc$ plays a crucial role in the theory of temporal logic and in algorithms for deciding properties like satisfiability, but it is rarely used to express properties of programs. In a concurrent program, not much can be said about what happens next since we don’t know which operation will be executed in the next step. Furthermore, we want a correctness statement to hold regardless of how the interleaving selects a next operation. Therefore, properties are almost invariably expressed in terms of always and eventually, not in terms of next.

• 运算符 $\bigcirc◯$ 在时间逻辑理论和决定可满足性等属性的算法中起着关键作用，但它很少被用来表达程序的属性。在一个并发程序中，对于下一步会发生什么并没有太多可说的，因为我们不知道下一步会执行哪个操作。此外，我们希望正确性声明总能够成立——不管交错如何选择下一个操作。因此，属性几乎都是用always和eventually来表达，而不是用next来表达**。

4. LTL

• In the context of programs, the natural interpretations of temporal logic formulas are discrete, reflexive, transitive and linear. There is another restriction that simplifies the presentation: the transition function must be total so that each state has exactly one next state. An interpretation for a computation that terminates in state s is assumed to have a transition from s to s.
  • 在程序的背景下，时间逻辑公式的自然解释是离散的、反射的、传递的和线性的。还有一个简化表述的限制：转换函数必须是完全的，以便每个状态正好有一个下一个状态 （即一一对应） 。一个终止于状态s的计算的解释被假定为有一个从s到s的过渡

---

• Linear temporal logic (LTL) is propositional temporal logic whose interpretations are limited to transitions which are discrete, reflexive, transitive, linear and total.
• Since there is only one transition out of each state, it need not be explicitly represented, so interpretations in LTL are defined to be paths of states
  • 也就是原来的状态转换$ρ:S→2^{S}$被省略了

• Let A be a formula in LTL. A is satisfiable iff there is an interpretation σ for A such that σ⊨A. A is valid iff for all interpretations σ for A, σ⊨A. Notation: ⊨A

• A formula of the form $\bigcirc A$ or $\lnot \bigcirc A$ is a next formula.

• A formula of the form $◊A$ or $¬ □A$ (‘eventually’ and ‘not always’) is a future formula.

• any substitution instance of a formula in propositional logic is also an LTL formula

• The method of semantic tableaux is a decision procedure for satisfiability in LTL

5. Binary Temporal Operators

• binary operator $\cap$ (read until)
  • The output lines maintain their values until the set-line is asserted
  • If A is $A_1 \cap A_2$ then $v_σ(A)=T$ iff $v_{σ_{i}}(A_2)=T$ for some $i≥0$ and for all $0≤k<i$, $v_{σ_k}(A_1)=T$

example

• $p \cap q$ is not true in the following interpretation assuming that state $s$ is repeated indefinitely:

• The Weak Until Operator
  • Sometimes it is convenient to express precedence properties without actually requiring that something eventually occur. $W$ (read weak until) is the same as the operator except that it is not required that the second formula ever become true