Practical First-Order Temporal Reasoning
Practical First-Order Temporal Reasoning
复制标题
实用一阶时序推理
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
A. Lisitsa
中科院分区：
文献类型：
--
作者：
C. Dixon;Michael Fisher;B. Konev;A. Lisitsa
在本文中，我们考虑了无限状态系统的时态逻辑描述和验证。特别是，我们使用一种新的一阶时态逻辑来描述参数化系统，这种逻辑既足够强大，可以用于这种形式的规范，又足够易于处理，可以用于实际的演绎验证。重要的是，时态语言的力量允许我们描述(和验证)异步系统、通信延迟以及更复杂的活跃性和公平性。对于无限状态验证的许多其他方法来说，这些方面似乎很困难。
In this paper we consider the specification and verification of infinite-state systems using temporal logic. In particular, we describe parameterised systems using a new variety of first-order temporal logic that is both powerful enough for this form of specification and tractable enough for practical deductive verification. Importantly, the power of the temporal language allows us to describe (and verify) asynchronous systems, communication delays and more complex liveness and fairness properties. These aspects appear difficult for many other approaches to infinite-state verification.