Model Checking Weighted Integer Reset Timed Automata

Weighted timed automata (WTA), introduced in Alur et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 49–62, Springer, Berlin, 2001), Behrmann et al. (Proceedings of HSCC’01, LNCS, vol. 2034, pp. 147–161, Springer, Berlin, 2001) are an extension of Alur and Dill (Theor. Comput. Sci. 126(2):183–235, 1994) timed automata, a widely accepted formalism for the modelling and verification of real time systems. Weighted timed automata extend timed automata by allowing costs on the locations and edges. There has been a lot of interest Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006), Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008), Brihaye et al. (Proceedings of FORMATS/FTRTFT’04, LNCS, vol. 3253, pp. 277–292, Springer, Berlin, 2004), Brihaye et al. (Inf. Comput. 204(3):408–433, 2006) in studying the model checking problem of weighted timed automata. The properties of interest are written using logic weighted CTL (WCTL), an extension of CTL with costs. It has been shown Bouyer et al. (Log. Methods Comput. Sci. 4(2):9, 2008) that the problem of model checking WTAs with a single clock using WCTL with no external cost variables is decidable, while 3 clocks render the problem undecidable Bouyer et al. (Inf. Process. Lett. 98(5):188–194, 2006). The question of 2 clocks is open. In this paper, we introduce a subclass of weighted timed automata called weighted integer reset timed automata (WIRTA) and study the model checking problem. We give a clock reduction technique for WIRTA. Given a WIRTA A\mathcal{A} with n≥1 clocks, we show that a single clock WIRTA A￠\mathcal{A}' preserving the paths and costs of A\mathcal{A} can be obtained. This gives us the decidability of model checking WIRTA with n≥1 clocks and m≥1 costs using WCTL with no external cost variables. We then show that for a restricted version of WCTL with external cost variables, the model checking problem is undecidable for WIRTA with 3 stopwatch costs and 1 clock. Finally, we show that model checking WTA with 2 clocks and 1 stopwatch cost against WCTL with no external cost variables is undecidable, thereby answering a question that has remained long open.     

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

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

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

自动机与模型检查

首先介绍自动机识别有限词和无限词两种情况,然后结合模型检查方法,把自动机作为规范自动机与模型自动机,使用自动机识别语言的包含问题技巧来解决模型检查问题,这里强调的是Vardi与Wolper提出的方法。     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

基于时间自动机的Web服务模型检测

传统的基于有限状态机的组合Web服务模型检测方法不能保证带有时间约束的组合Web服务的正确性.把组合Web服务看成多智能体系统,将带有时间约束的Web服务智能体建模为时间自动机,通过并发组合构成时间自动机网络,从而用时间自动机验证工具UPPAAL对组合Web服务的运行过程进行模拟,并验证其活性、安全性和死锁等性质.采用该方法对雇员出差安排组合Web服务进行建模和验证,结果表明,该组合Web服务存在死锁问题.最后通过分析死锁产生的路径,完善该组合Web服务的通信协议,从而消除了死锁.     

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

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

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.     

Weighted Picture Automata and Weighted Logics

We investigate formal power series on pictures. These are functions that map pictures to elements of a semiring and provide an extension of two-dimensional languages to a quantitative setting. We establish a notion of a weighted MSO logics over pictures. The semantics of a weighted formula will be a picture series. We introduce weighted 2-dimensional on-line tessellation automata (W2OTA) and prove that for commutative semirings, the class of picture series defined by sentences of the weighted logics coincides with the family of picture series that are computable by W2OTA. Moreover, we show that the family of behaviors of W2OTA coincide precisely with the class of picture series characterized by weighted (quadrapolic) picture automata and consequently, the notion of weighted recognizability presented here is robust. However, the weighted structures can not be used to get better decidability properties than in the language case. For every commutative semiring, it is undecidable whether a given MSO formula has restricted structure or whether the semantics of a formula has empty support.     

Weighted Logics for Unranked Tree Automata

We define a weighted monadic second order logic for unranked trees and the concept of weighted unranked tree automata, and we investigate the expressive power of these two concepts. We show that weighted tree automata and a syntactically restricted weighted MSO-logic have the same expressive power in case the semiring is commutative or in case we deal only with ranked trees, but, surprisingly, not in general. This demonstrates a crucial difference between the theories of ranked trees and unranked trees in the weighted case.     

A Kleene Theorem for Weighted Tree Automata

In this paper we prove Kleenes result for formal tree series over a commutative semiring A (which is not necessarily complete or continuous or idempotent), i.e., the class of formal tree series over A which are accepted by weighted tree automata, and the class of rational tree series over A are equal. We show the result by direct automata-theoretic constructions and prove their correctness.     

Checking Finite Traces Using Alternating Automata

Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a linear-time temporal logic formula. The three methods start from the same alternating automaton but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. We then show how an extension of these algorithms, that collects statistical data while verifying the execution trace, can be used for a more detailed analysis of the runtime behavior. All three methods have been implemented and experimental results are presented.     

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.     

赋权型自动机的不同模型研究

自动机理论是理论计算机科学的基础理论之一,在很多领域自动机有着广泛的应用,有穷状态自动机是正则语言的识别机器,通常分为确定型与非确定型两种模型,其识别语言的能力是等价的。赋权自动机是另一类重要的自动机模型,自动机的每条转移规则和状态可以赋以某一代数结构上的某一数值,从而可以计算输入字符串的权值。任何有穷状态自动机都可以视为一特殊赋权自动机,因此赋权自动机功能更强大,应用更为广泛。     

An Approximate Determinization Algorithm for Weighted Finite-State Automata

Nondeterministic weighted finite-state automata are a key abstraction in automatic speech recognition systems. The efficiency of automatic speech recognition depends directly on the sizes of these automata and the degree of nondeterminism present, so recent research has studied ways to determinize and minimize them, using analogues of classical automata determinization and minimization. Although, as we describe here, determinization can in the worst case cause poly-exponential blowup in the number of states of a weighted finite-state automaton, in practice it is remarkably successful. In extensive experiments in automatic speech recognition systems, deterministic weighted finite-state automata tend to be smaller than the corresponding nondeterministic inputs. Our observations show that these size reductions depend critically on the interplay between weights and topology in nondeterministic weighted finite-state automata. We exploit these observations to design a new approximate determinization algorithm, which produces a deterministic weighted finite-state automaton that preserves the strings of a weighted language but not necessarily their weights. We apply our algorithm to two different types of weighted finite-state automata that occur in automatic speech recognition systems and in each case provide extensive experimental results showing that, compared with current techniques, we achieve significant size reductions without affecting performance. In particular, for a standard test bed, we can reduce automatic speech recognition memory requirements by 25—35\percent with negligible effects on recognition time and accuracy. Received March 31, 1998; revised January 29, 1999.     

有限精度时间自动机的可达性检测

为了缓解状态空间爆炸问题,减小模型检测过程中生成的状态空间,加快模型检测速度,引入有限精度时间自动机(finite precision timed automata,简称FPTA)作为实时系统的形式模型,并提出了一种数据结构SDS(series of delay sequence)符号化表示状态空间中的状态集.FPTA只记录时钟变量的整数值及时钟变化的先后次序,从而减小生成的状态空间.在一定的时间约束下,Alur与Dill提出的时间自动机的可达性检测可简化为FPTA的可达性检测.举例描述了状态空间的生成过程和表示方法.最后,列出部分初步的实验结果,分析了SDS的特点及不足.     

基于关系模型的UML类图一致性检验

UML类图是UML建模语言的核心元素之一,类图模型的正确性和一致性对于保证需求分析的正确性至关重要。论文研究了UML类图模型的语义一致性问题,提出了一种自动检验类图一致性的方法。该方法以扩展的关系逻辑为语义基础,把一致性问题归结为关系逻辑公式的可满足性问题。实践表明,该方法能够有效的检查UML类图模型的一致性,发现需求分析中的错误和漏洞,在一定程度上保证了类图模型的正确性。     

一种基于时间自动机的实时系统模型检查算法的设计与实现

该文首先简介了时间自动机、时钟区域、区域等价、时钟带的概念,利用区域等价关系,可以将时间自动机的无穷状态空间转化为有穷。然后通过一个典型的实例完整地介绍了基于时间自动机的实时系统模型检查技术,并用Visual C++语言描述了实时特性验证中的数据结构,实现了实时特性验证算法,实验表明利用该算法可以进行实时系统的形式化验证。     

基于Uppaal的时延Petri网到时间自动机等价模型验证*

时延Petri网和时间自动机都可以有效地对实时系统的行为进行模拟和性能分析。利用时延Petri网到时间自动机等价转换算法（简记作TPN-to-TA 转换）,将一个描述实时系统的时延Petri网模型转换成与其语义等价的一组时间自动机模型。使用时间自动机中成熟的模型验证工具Uppaal对此时延Petri网的模型进行验证。