Failure diagnosis of discrete-event systems with linear-time temporal logic specifications

The paper studies failure diagnosis of discrete-event systems (DESs) with linear-time temporal logic (LTL) specifications. The LTL formulas are used for specifying failures in the system. The LTL-based specifications make the specification specifying process easier and more user-friendly than the formal language/automata-based specifications; and they can capture the failures representing the violation of both liveness and safety properties, whereas the prior formal language/automaton-based specifications can capture the failures representing the violation of only the safety properties (such as the occurrence of a faulty event or the arrival at a failed state). Prediagnosability and diagnosability of DESs in the temporal logic setting are defined. The problem of testing prediagnosability and diagnosability is reduced to the problem of model checking. An algorithm for the test of prediagnosability and diagnosability, and the synthesis of a diagnoser is obtained. The complexity of the algorithm is exponential in the length of each specification LTL formula, and polynomial in the number of system states and the number of specifications. The requirement of nonexistence of unobservable cycles in the system, which is needed for the diagnosis algorithms in prior methods to work, is relaxed. Finally, a simple example is given for illustration.     

Diagnosis of repeated failures for discrete event systems with linear-time temporal-logic specifications

In our earlier work, we introduced a state-based approach for the diagnosis of repeatedly occurring failures in discrete event systems (DESs). Since temporal logic provides a simpler way of specifying system properties; in this paper, a temporal-logic-based approach for diagnosing the occurrence of a repeated number of failures is developed. Linear-time temporal-logic (LTL) formulae are used to represent the specifications of DESs. Notions of prediagnosability for failures and diagnosability for repeated failures are introduced in the setting of temporal logic. A polynomial algorithm for the test of prediagnosability for failures is provided. The diagnosis problem for repeated failures in the temporal-logic setting is reduced to one in a state-based setting, and so the prior results of a state-based repeated failure diagnosis can be applied. Finally, a simple example is given for illustration. Note to Practitioners-Certain failures in a system are repeatable, such as routing errors in a manufacturing system. A theory for the diagnosis of such failures was presented in an earlier work of Jiang et al. The present paper uses temporal logic to specify such failures. It turns out that repeatable failures can be specified as violations of invariant properties (i.e., properties that must always hold). Given an invariant property that the system must always satisfy, an algorithm is presented to refine the system model and label those states of the refined system where the property is violated. The problem of repeated diagnosis then requires determining, within a bounded delay, each time a "failure-state" is visited. For this analysis, the existing theory developed by Jiang et al. is used.     

Efficient approach of translating LTL formulae into Büchi automata

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).     

Efficient approach of translating LTL formulae into Büchi automata

In explicit-state model checking, system properties are typically expressed in linear temporal logic (LTL), and translated into a Büchi automaton (BA) to be checked. In order to improve performance of the conversion algorithm, some model checkers involve the intermediate automata, such as a generalized Büchi automaton (GBA). The de-generalization is a translation from a GBA to a BA. In this paper, we present a conversion algorithm to translate an LTL formula to a BA directly. A labeling, acceptance degree, is presented to record acceptance conditions satisfied in each state and transition. Acceptance degree is a set of U-subformulae or F-subformulae of the given LTL formula. According to the acceptance degree, on-the-fly degeneralization algorithm, which is different from the standard de-generalization algorithm, is conceived and implemented. On-the-fly de-generalization algorithm is carried out during the expansion of the given LTL formula. It is performed in the case of the given LTL formula contains U-subformulae and F-subformulae, that is, the on-the-fly de-generalization algorithm is performed as required. In order to get a more deterministic BA, the shannon expansion is used recursively during expanding LTL formulae. Ordered binary decision diagrams are used to represent the BA and simplify LTL formulae.We compare the conversion algorithm presented in this paper to previousworks, and show that it is more efficient for five families LTL formulae in common use and four sets of random formulae generated by LBTT (an LTL-to-Büchi translator testbench).     

QRDChecker:一个QRDC模型检验工具

反应式系统通常是不终止的,其行为定义为系统状态的无限序列的集合.形式化验证时,检验需求一般使用时序逻辑给出.当使用诸如LTL(linear temporal logic)这样的逻辑时,由于这类逻辑的模型同样是无限序列,系统与需求之间的满足性关系可以简单定义为集合的包含关系.但是,当使用时段时序逻辑(interval temporal logic)作为说明逻辑时,由于逻辑模型的有限性,使得上面的满足关系不再适用.称这类有限序列集合表达的性质为有限性性质.对于不同的有限性性质,它们对应的满足性关系是有区别的.针对两类有限性定义了它们各自的满足性关系,并将这两种关系统一为一个更一般的满足性关系.在此基础上,提出模型检验这两类性质的算法,并将其实现为一个针对时段时序逻辑QRDC(quantified RDC (restricted duration calculus))的检验工具QRDChecker.QRDChecker可以检验QRDC公式在连续时间模型和离散时间模型下的有效性.在离散时间条件下,它还可以将QRDC公式转换成模型检验系统Spin能够接受的自动机的形式,从而可以检查反应式系统是否满足用QRDC公式表达的性质.     

LTL公式到自动机的转换

在LTL公式和自动机理论的基础上,给出了一种从LTL公式到自动机的转换算法.该算法先简化LTL公式,然后再对简化的LTL公式转换,形成选择Buchi自动机.此算法与其他算法相比,具有可扩展性的优点,可以在此基础上形成属性描述语言PSL向自动机的转换.     

可能性测度下的LTL模型检测并行化研究

分布式模型检测是一种缓解状态空间爆炸的有效途径,已有文献提出了定性的分布式模型验证算法,然而定量LTL验证算法并行化问题还未得到有效解决。对此,展开两个方面的工作:提出一种新的动态系统状态空间划分方法;在定性LTL分布式验证算法的基础上给出了定量模型检测并行化验证算法。首先,将系统模型转化为可能的Kripke结构并选取一个并发分量,依据状态之间的关系完成系统状态的分割,使得关系紧密的状态尽可能分布在同一个计算节点上;其次,调整划分结果以使得计算负载平衡;然后,将划分结果与其他并发分量的状态进行叉乘,以完成系统状态空间的划分;最后,将待检测性质用自动机表示,在两者的乘积上,利用扩展的基于嵌套DFS的分布式验证算法完成系统的定量验证。     

从基于迁移的扩展Büchi自动机到Büchi自动机

目前的模型检测方法中,有一种方法是基于自动机来实现的.具体做法是:将抽象出的系统模型用Büchi自动机来表示,将需要验证的性质用LTL(linear temporal logic)公式来表达;然后将LTL公式取反后转化为Büchi自动机,并检查这两个自动机接受语言之间的包含关系.有一类LTL公式转化为Büchi自动机的算法是:在计算过程中,首先得到一个标注在迁移上的扩展Büchi自动机(transition-based generalized Büchi automaton,简称TGBA),然后把这种扩展Büchi自动机转换成非扩展的Büchi自动机.针对这类转换算法,根据Büchi自动机接受语言的特点,重新定义了基于迁移的扩展Büchi自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.     

基于ASP的CSP并发系统验证研究

传统并发通信顺序进程(CSP>性质的验证通常使用3个不同的模型层面,从而增加了系统的复杂性和验证 工具开发的难度;同时,主流的并发系统模型验证工具不支持在系统的一次运行中验证多个性质,这也降低了性质验 证的效率。首先将CSP程序转换为ASP程序,然后将CSP进程并发规则和以LTL/CTL公式表示的待验证性质转 换为ASP规则,从而建立了基于ASP验证CSP并发系统性质的统一框架。实验结果表明,基于ASP的CSP并发系 统验证技术易于实现,在保持较高验证效率的同时,能够支持在验证软件的一次执行中验证多条LTL/CTL公式。     

Symbolic systems,explicit properties: on hybrid approaches for LTL symbolic model checking

In this work we study hybrid approaches to LTL symbolic model checking; that is, approaches that use explicit representations of the property automaton, whose state space is often quite manageable, and symbolic representations of the system, whose state space is typically exceedingly large. We compare the effects of using, respectively, (i) a purely symbolic representation of the property automaton, (ii) a symbolic representation, using logarithmic encoding, of explicitly compiled property automaton, and (iii) a partitioning of the symbolic state space according to an explicitly compiled property automaton. We apply this comparison to three model-checking algorithms: the doubly-nested fixpoint algorithm of Emerson and Lei, the reduction of emptiness to reachability of Biere et al., and the singly-nested fixpoint algorithm of Bloem et al. for weak automata. The emerging picture from our study is quite clear, hybrid approaches outperform pure symbolic model checking, while partitioning generally performs better than logarithmic encoding. The conclusion is that the hybrid approaches benefit from state-of-the-art techniques in semantic compilation of LTL properties. Partitioning gains further from the fact that the image computation is applied to smaller sets of states.     

程序时序属性的自动测试

测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中，作者设计并实现了一种根据程序的线性时序逻辑(LTL)的性质产生测试预言的方法。首先，作者将一线性时序逻辑公式转换为一个有限状态自动机，然后，管理源代码，以便抽取与线性时序逻辑性质有关的状态序列。最后，用谊信息来模拟状态自动机，并决定程序执行是否满足线性时序逻辑的性质。     

Vectorial languages and linear temporal logic

Determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. The main difficulty is to do this computation efficiently. Considering words as vectors and working on them using vectorial operations allows to solve the problem faster than using local operations.

In this paper, we show first that the set of vectorial operations needed by an algorithm representing a given automaton depends on the language accepted by the automaton. We give precise characterizations for star-free, solvable and regular languages using vectorial algorithms. We also study classes of languages associated with restricted sets of vectorial operations and relate them with languages defined by fragments of linear temporal logic.

Finally, we consider the converse problem of constructing an automaton from a given vectorial algorithm. As a byproduct, we show that the satisfiability problem for some extensions of LTL characterizing solvable and regular languages is PSPACE-complete.     

Tableau-based automata construction for dynamic linear time temporal logic*

We present a tableau-based algorithm for obtaining a Büchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Büchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.*This research has been partially supported by the project MIUR PRIN 2005 ‘Specification and verification of agent interaction protocols’.     

线性时序逻辑引导的安全强化学习

针对动态不确定环境下机器人执行复杂任务的需求,提出一种线性时序逻辑(linear temporal logic, LTL)引导的无模型安全强化学习算法,能在最大化任务完成概率的同时保证学习过程的安全性.首先,综合考虑环境中的不确定因素,构建马尔可夫决策过程(Markov decision process, MDP),再用LTL刻画智能体的复杂任务,将其转化为有多接受集的基于转移的有限确定性广义布奇自动机(transition-based limit deterministic generalized Büchi automaton, t LDGBA),并通过接受边界函数构建可记录当前待访问接受集的约束型tLDGBA (constrained tLDGBA,ctLDGBA);其次,构建乘积MDP用于强化学习搜索最优策略;最后,基于LTL对安全性的描述和MDP的观测函数构建安全博弈,并根据安全博弈设计安全盾机制保证系统在学习过程中的安全性.严格的分析证明了所提出的算法能获得最大化LTL任务完成概率的最优策略.仿真结果验证了LTL引导的安全强化学习算法的有效性.     

Computing observers from observation policies in discrete-event systems

This paper considers partially-observed discrete-event systems modeled by finite-state automata. The observation of event occurrences is associated with the transitions of the automaton model. That is, whether or not an event occurrence is observed is state-dependent, i.e., it depends on the transition in which the event label appears. This is in contrast to the case when observations are static and an event is either observed or not observed at every state in which it can occur. We refer to the set of transitions whose associated events are observed as an observation policy. Given an automaton model and an observation policy, we consider the problem of computing a deterministic generator of the language of event sequences that are observed using the automaton model and observation policy (i.e., an observer). Such a generator is useful, e.g., in problems of sensor activation for providing a deterministic mapping from event observations to sensor activation decisions when the decision to activate an event’s sensor is initially modeled as an observation policy. We propose an abstraction of the automaton model that may be used to represent an observer in certain cases. We illustrate cases where this abstraction accurately represents an observer when there is no ambiguity as to which event occurrences are observed following two observationally-identical strings. For the most general case considered, we demonstrate that verifying if the case holds is PSPACE-complete.     

格值有限状态自动机的同态和商自动机

提出了格值有限状态自动机（LFSA）的同态、强同态的概念,研究了LFSAs同态、强同态的若干性质。在LFSAs强同态的基础上,得到了LFSA的商自动机及其最小化自动机,刻画了商自动机的性质。     

On Closure Under Stuttering

For over a decade, researchers in formal methods have tried to create formalisms that permit natural specification of systems and allow mathematical reasoning about their correctness. The availability of fully automated reasoning tools enables non-experts to use formal methods effectively—their responsibility reduces to specifying the model and expressing the desired properties. Thus, it is essential that these properties be represented in a language that is easy to use, sufficiently expressive and succinct. Linear-time temporal logic (LTL) is a formalism that has been used extensively by researchers for program specification and verification. One of the desired properties of LTL formulas is closure under stuttering. That is, we do not want the interpretation of formulas to change over traces where some states are repeated. This property is important from both practical and theoretical prospectives; all properties which are closed under stuttering can be expressed in LTL_–X—a fragment of LTL without the next operator. However, it is often difficult to express properties in this fragment of LTL. Further, determining whether a given LTL property is closed under stuttering is PSPACE-complete. In this paper, we introduce a notion of edges of LTL formulas and present a formal theory of closure under stuttering. Edges allow natural modelling of systems with events. Our theory enables syntactic reasoning about whether the resulting properties are closed under stuttering. Finally, we apply the theory to the pattern-based approach of specifying temporal formulas.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

Contract as automaton: representing a simple financial agreement in computational form

We show that the fundamental legal structure of a well-written financial contract follows a state-transition logic that can be formalized mathematically as a finite-state machine (specifically, a deterministic finite automaton or DFA). The automaton defines the states that a financial relationship can be in, such as “default,” “delinquency,” “performing,” etc., and it defines an “alphabet” of events that can trigger state transitions, such as “payment arrives,” “due date passes,” etc. The core of a contract describes the rules by which different sequences of events trigger particular sequences of state transitions in the relationship between the counterparties. By conceptualizing and representing the legal structure of a contract in this way, we expose it to a range of powerful tools and results from the theory of computation. These allow, for example, automated reasoning to determine whether a contract is internally coherent and whether it is complete relative to a particular event alphabet. We illustrate the process by representing a simple loan agreement as an automaton.

     

The Variable Hierarchy of the μ-Calculus Is Strict

Most of the logics commonly used in verification, such as LTL, CTL, CTL^*, and PDL can be embedded into the two-variable fragment of the μ-calculus. It is also known that properties occurring at arbitrarily high levels of the alternation hierarchy can be formalised using only two variables. This raises the question of whether the number of fixed-point variables in μ-formulae can be bounded in general. We answer this question negatively and prove that the variable-hierarchy of the μ-calculus is semantically strict. For any k, we provide examples of formulae with k variables that are not equivalent to any formula with fewer variables. In particular, this implies that Parikh's Game Logic is less expressive than the μ-calculus, thus resolving an open issue raised by Parikh in~1983.