线性时序逻辑模型检测

原文放在     
线性时序逻辑（Linear Temporary Logic, 简称 LTL）是命题逻辑的基础上加了几个算子（Next P,     P until Q,    Eventually P,       Always P）。 

线性时序逻辑因用于程序模型检测而出名。下面用Python编程演示简单的模型检测例子。

#coding=utf-8
class Node: #定义节点类
  def __init__(self,v,name):
    self.v=v  #节点的值
    self.next=None #节点的后继
    self.name=name #节点的名称
    self.path=[] #从开始到此节点的路径

A=Node(3,'A')   #节点 ‘A’
B=Node(3,'B')  #节点 ‘B’
C=Node(5,'C')  #节点‘C’
A.next=B
B.next=C

现在我们给出两个原子公式 p 和 q；  p：该节点的值等于3，   q：该节点的值是偶数

def p(n):
  if n.v>=3: return True  #是否等于3
  else: return False
def q(n):
  if n.v%2==0: return True  #是否是偶数
  else: return False

我们现在要检验的性质是：  “从A出发，是否一直等于3，直到是一个偶数为止。”  
有点拗口，换句说法：“ 从A出发，如果不出现偶数，就一直是等于3，是不是？”

用线性时序逻辑表达为： p U q,   或   p until q ，
其语义用Python程序表达出来，就能作为检测用的函数：

"""
p until q:    p直到q

There must be an N such that q(N) is True, and that
for each n

"""
def pUq(n):
  if not p(n) and not q(n):    # 还未出现q,    p就不成立了， 返回假
    print n.name,n.path,'Nonsence!'
    return False
  elif q(n):  #已经出现q,  返回真
    print n.name,n.path,'It happens!'
    return True
  elif not q(n) and n.name in n.path:   # 还没出现q, 但前面路径里已出现过该节点说明这里有个环，
    print n.name,n.path,'Loop detected!' #  如此重复环下去，一直没有q, 所以返回假
    return False
  elif not n.next:      #以上情况都不满足，但该节点已没有后继，返回假
    print n.name,n.path,'Deadlock'
    return False
  else:   #以上情况都不满足，还需要检查其后继节点是否满足该性质
    n.next.path.extend(n.path+[n.name])
    return pUq(n.next)

print pUq(A)  #执行检查，从节点A开始

线性时序逻辑模型检测并非不能用于分支结构。没有计算树逻辑的路径算子（所有路径，某条路径），某个节点满足某公式， 意思就是从此节点开始的所有路径都满足此公式。
所以，如果是分支结构，即某些节点的后继节点有多个，可以修改Node的next属性为列表，并把pUq中else分支修改为：

map(lambda c: c.path.extend(n.path+[n.name]), n.next)
return all(map(pUq,n.next))

 
因为其它几个算子都比较容易（Next p 表示后继节点满足p,   Eventually p 就是 True Until p,   Always p 就是 not Eventually not p ）,  读者可以自己试着写出来。这里不再赘述。

注意，假如碰到要检测节点n是否满足 “如果p那么q”,  以及 “p 或者 q”,  这里p和q可能是原子公式也可能不是。那么，不要转化为 not p(n) or q(n)， 以及 p(n) or q(n).  而是用反证法去检测：前者对p(n) and not q(n)返回假，否则返回真； 后者对 not p(n) and not q(n) 返回真，否则为假。
原因是：如前面提到的，某节点满足P表示所有路径满足P，某节点满足 PUQ，并不是说该节点的所有路径满足P，或者所有路径满足Q，而是说一部分路径满足P，剩下的满足P。所以你需要用反证法。

另外，如果你要寻找一条符合特定性质的路径，就把这条性质反着输进入。原因还是上面说的。模型检测是在说某个节点出发的所有路径是否符合某性质。 反着检测，错了，它会给你反例路径；对了，表示没有你要找的路径。

最后要说的是无穷多的状态怎么办？ 模型检测本来对于无穷多状态问题是半判定的，即：如果某性质是错的，则可能碰到错误并返回，如果是对的，则肯定永远无法返回。