Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

Checking Finite Traces using Alternating Automata

We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a future linear-time temporal logic formula. The three methods are all based on alternating automata, but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. All three methods have been implemented and experimental results are presented. We outline an extension to these algorithms that is applicable to LTL formulas containing both past and future operators.     

Bounded Model Checking with SNF,Alternating Automata,and Büchi Automata

Model checking of LTL formulæis traditionally carried out by a conversion to Büchi automata, and there is therefore a large body of research in this area including some recent studies on the use of alternating automata as an intermediate representation.Bounded model checking has until recently been apart from this, typically using a direct conversion from LTL to propositional logic. In this paper we give a new bounded model checking encoding using alternating automata and focus on the relationship between alternating automata and SNF. We also explore the differences in the way SNF, alternating, and Büchi automata are used from both a theoretical and an experimental perspective.     

How to Verify a Safe Real-Time System: The Application of Model Checking and Timed Automata to the Production Cell Case Study*

The formal verification of a real-time system requires either a proof theoretic or model theoretic approach. Both being applicable to a model of the proposed behavior of the concurrent real-time system. This paper evaluates the use model checking and timed automata by their application to an adaptation of the Production Cell case study. The Uppaal tool is used in this evaluation. The modeling aspects were found to be straightforward, but to accomplish the necessary model checking required some knowledge of the underlying process. Nevertheless, the conclusion of the study is that these techniques are generally applicable and be can be undertaken in an engineering context without detailed domain knowledge of the model checking technique.     

Another Look at LTL Model Checking

We show how LTL model checking can be reduced to CTL model checking with fairness constraints. Using this reduction, we also describe how to construct a symbolic LTL model checker that appears to be quite efficient in practice. In particular, we show how the SMV model checking system developed by McMillan [16] can be extended to permit LTL specifications. The results that we have obtained are quite surprising. For the specifications which can be expressed in both CTL and LTL, the LTL model checker required at most twice as much time and space as the CTL model checker. We also succeeded in verifying non-trivial LTL specifications. The amount of time and space that is required is quite reasonable. Based on the examples that we considered, it appears that efficient LTL model checking is possible when the specifications are not excessively complicated.     

时间自动机的LTL性质模型检测研究

为了增强模型检测工具的检测能力,拓宽模型检测技术的应用范围,对基于时间自动机的LTL性质模型检测进行了研究,对自动机的状态空间的存储方式和状态空间的展开过程进行了分析,讨论了LTL性质模型检测工具的检测流程和检测算法的实现策略对工具检测性能的影响,针对制约模型工具的检测能力和检测效率的因素,采取了一些相应的优化改进策略.采用了BDD(二叉决策图)共享存储技术和位编码压缩存储,较有效地减小了空间消耗,缓解了模型检测中状态爆炸引起的内存空间不足问题.与DTSpin等著名的模型检测工具进行了实验比较,取得了较好的实验结果.     

Collecting Statistics Over Runtime Executions

We present an extension to linear-time temporal logic (LTL) that combines the temporal specification with the collection of statistical data. By collecting statistics over runtime executions of a program we can answer complex queries, such as “what is the average number of packet transmissions' in a communication protocol, or “how often does a particular process enter the critical section while another process remains waiting' in a mutual exclusion algorithm. To decouple the evaluation strategy of the queries from the definition of the temporal operators, we introduce algebraic alternating automata as an automata-based intermediate representation. Algebraic alternating automata are an extension of alternating automata that produce a value instead of acceptance or rejection for each trace. Based on the translation of the formulas from the query language to algebraic alternating automata, we obtain a simple and efficient query evaluation algorithm. The approach is illustrated with examples and experimental results.     

一种基于离散时间自动机的LTL性质检测工具

模型检测是一种自动完成性质验证的算法过程,在模型检测过程中会遇到状态空间爆炸的问题,即随系统规模的增长状态空间的大小呈指数增长,如何缓解此问题一直是研究者研究的重点.目前利用模型检测方法对线性时序逻辑(LTL)性质进行检测的工具还比较少,且效率都较低.介绍了一种基于离散时间自动机的LTL性质检测工具,采用了在状态空间中存储延迟序列(DS)的技术,对状态进行压缩存储,减小了时间空间的消耗,加快了检测速度.实验表明,该工具的检测效果是不错的,要好于同类工具,如DTSpin.     

Efficient Detection of Vacuity in Temporal Model Checking

The ability to generate a counter-example is an important feature of model checking tools, because a counter-example provides information to the user in the case that the formula being checked is found to be non-valid. In this paper, we turn our attention to providing similar feedback to the user in the case that the formula is found to be valid, because valid formulas can hide real problems in the model. For instance, propositional logic formulas containing implications can suffer from antecedent failure, in which the formula is trivially valid because the pre-condition of the implication is not satisfiable. We call this vacuity, and extend the definition to cover other kinds of trivial validity. For non-vacuously valid formulas, we define an interesting witness as a non-trivial example of the validity of the formula. We formalize the notions of vacuity and interesting witness, and show how to detect vacuity and generate interesting witnesses in temporal model checking. Finally, we provide a practical solution for a useful subset of ACTL formulas.     

基于Verics的组合Web服务有界模型检测

传统的模型检测技术无法描述系统的认知逻辑特性,而在分布式系统领域,系统和协议的规范适合用多智能体时态认知逻辑来描述.组合Web服务是典型的分布式系统.为了保证组合Web服务运行的正确性,把组合Web服务看成多智能体系统,将其建模成一组相互通信的时间自动机.采用时态认知逻辑模型检测工具Verics对该组合Web服务的可用性、可靠性和时效性的时态认知逻辑特性进行检测.本文以旅游预订系统组合Web服务为例,阐述了上述过程.