时间逻辑
维基百科，自由的百科全书
在逻辑中，术语时间逻辑被用来描述为表现和推理关于时间限定的命题的规则和符号化的任何系统。它有时也被称为时态逻辑，这是 Arthur Prior 在1960年代介入的基于模态逻辑的特殊的时间逻辑系统。它后来被计算机科学家特别是 Amir Pnueli 和逻辑学家进一步的开发。
时间逻辑首先被亚里士多德深入研究过，他的著作中有粗糙形式的一阶时间模态二值逻辑。使用存在量词或全称量词的任何逻辑都叫做一阶逻辑。把时间看作状态的序列的任何逻辑都是时间逻辑，只使用两个真值的任何逻辑都是二值逻辑。
考虑陈述: "我饿了"。尽管它的意思随时间恒定，但这个陈述的真值随时间可变。有时这个陈述为真，有时这个陈述为假，但是这个陈述不能同时为真并且为假。在时间逻辑中，陈述可以有随时间变化的真值。与之相对的是非时间逻辑，它只能处理有着随时间恒定的真值的陈述。
三个基本时间算子是: 总是、有时、和永不。
计算树逻辑(CTL)、线性时间逻辑(LTL)和间隔时间逻辑(ITL)是时间逻辑的例子。
[编辑] 参见
- 持续时间演算 (DC)
- 混合逻辑
- 间隔时间逻辑
- 有限状态验证中的时间逻辑
- 动作的时间逻辑 (TLA)
- 在形式验证中重要出版物(包括在形式验证中时间逻辑的使用)
