从基于迁移的扩展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自动机的求交运算,减少了需要复制的状态个数,使转换后的自动机具有较少的状态.测试的结果表明:对随机产生的公式,新算法相对于以往的算法有明显的优势.     

一种有效的基于LTL和Petri网的模型检测方法

模型检测的一个主要方法是构建线性与时序逻辑（LTL）公式φ的否定形式等价的Büchi自动机Aφ和系统模型M的正交积，并检测正交积的可接受语言是否为空。通过对Generalized Büchi自动机进行化简，可以减小自动机的状态空间，从而提高模型检测的效率。根据所提出的方法设计并实现的基于LTL和Petri网进行模型检测的工具包，可以有效地对基于Petri网表示的系统模型进行模型检测。     

基于EHA模型检验Statecharts

模型检验是一种重要的形式化自动验证技术。Statecharts是一种用以规约复杂反应式系统行为的可视化语言。为了验证Statecharts模型是否满足所期望的性质,该文给出了一种基于EHA模型检验Statecharts的方法,首先把Statecharts转换为EHA,通过其操作语义得到Büchi自动机,然后与LTL公式所得的Büchi自动机相乘,最后检查该乘积自动机所能接受的语言是否为空,来判断是否满足所期望的性质。     

APTL公式的可满足性检查工具

交替投影时序逻辑（Alternating Projection Temporal Logic,简称APTL）公式简单易懂,表达能力强;不仅可以描述经典时序逻辑LTL可以描述的性质,而且可以描述与区间相关的顺序和循环性质以及开放系统和多智能体系统中与博弈相关的性质.在验证系统是否满足所给的APTL公式所描述的性质之前需要检查公式的可满足性.本文根据检查APTL公式的可满足性的方法^[1],开发实现了工具APTL2BCG.具体细节如下：首先,利用公式P的范式构造P的标记范式图（Labeled Normal Form Graph,简称LNFG）;然后,将LNFG转化为广义的基于并发博弈结构的交替Büchi自动机（Generalized alternating Büchi automaton over Concurrent Game structure,简称GBCG）;最后,将GBCG转化为基于并发博弈结构的交替Büchi自动机（alternating Büchi automaton over Concurrent Game structure,简称BCG）并且化为最简形式并检查公式P的可满足性.     

Büchi自动机确定化分析工具

无限字自动机的确定化是理论计算机研究重要的一部分,在形式化验证,时序逻辑,模型检测等方面有重要应用.自Büchi自动机提出半个世纪以来,其自动机的确定化算法始终是其中的基础.有别于当初只是在理论上对其大小上下界的探索,利用日新月异的高性能计算机技术不失为一种有效的辅助手段.为了深入研究非确定性Büchi自动机确定化算法的实现过程,我们希望重点研究确定化过程中的索引能否继续被优化的问题,实现了确定化研究工具NB2DR.可以对非确定性Büchi自动机进行高效的确定化,并通过工具提供的分析其确定化过程来达到对其确定化算法改进的目的.通过对生成的确定性无限字自动机的索引的深入分析来探索相关索引的理论.该工具还实现了可以根据需要的Büchi自动机的大小与字母表参数,生成确定化的Rabin自动机族,亦可以反向根据需要的指定索引的大小来生成全部Büchi自动机族,测试生成无限字自动机的等价性等功能.     

一种利用非确定规划的LTL合成方法

LTL合成(Linear Temporal Logic synthesis)是程序合成(program synthesis)的一类重要子问题, 旨在自动构建一个控制器(controller), 且要求该控制器和环境(environment)的行为交互满足给定的LTL公式.一般来说, 可以将LTL合成定义为二人博弈(two-player game)问题, 博弈的双方是环境和控制器, 该问题的解称为合成策略.近年来, 有研究从理论角度讨论了LTL合成与非确定规划(non-deterministic planning)的相关性.基于此, 本文提出了一种新的利用非确定规划求解LTL合成问题的方法, 并证明了方法的正确性和完备性.具体而言, 首先获得LTL公式对应的Büchi自动机, 结合二人博弈定义, 将LTL合成问题转换为完全可观测的非确定规划模型, 然后交由高效规划器求解.通过实验结果说明, 与其他LTL合成方法相比, 本文提出的基于规划的合成方法在解质量方面具有较大的优势, 能够获得规模较小的合成策略.     

矩阵前主子式的三角分解改进

采用部分主元素的Gauss消去法一般不能得到矩阵的各阶前主子式。讨论围绕逐步约化的细分每小步,对一个经过若干行置换后的A0最后实现三角分解,并且依顺序求出A₀各阶前主子式。主要内容是对带有行交换三角形化的通常约化方法实现改进,并以代数表示式结合矩阵乘积运算的递推方法,归纳证明最后约化结果式子为矩阵L-U三角分解的实现依据。逐步约化步骤的同时得到原有矩阵A₀的各阶前主子式。     

P2-Packing问题参数算法的改进

P₂-Packing问题是一个典型的NP难问题.目前这个问题的最好结果是时间复杂度为O^*(2^5.301k)的参数算法,其核的大小为15k.通过对P₂-packing问题的结构作进一步分析,提出了改进的核心化算法,得到大小为7k的核,并在此基础上提出了一种时间复杂度为O^*(2^4.142k)的参数算法,大幅度改进了目前文献中的最好结果.     

正则化和交叉验证在组合预测模型中的应用

组合预测模型的权重确定方式对于提高模型精度至关重要,为研究正则化与交叉验证是否能改善组合预测模型的预测效果,提出将正则化和交叉验证应用于基于最小二乘法的组合预测模型.通过在组合模型的最优化求解中分别加入L₁、L₂范数正则化项,并对数据集进行留一交叉验证后发现：L₁、L₂范数正则化都对组合模型的预测精度具有改善效果,且L₁范数正则化比L₂范数正则化对组合预测模型的改善效果更好,并且参与组合预测的单项预测模型越多,正则化的改善效果越好,交叉验证对组合预测模型的改善效果则与给定实验数据量呈现正相关.     

线性动态系统反演模型在人体行为识别的应用

目的 人体行为识别在视频监控、环境辅助生活、人机交互和智能驾驶等领域展现出了极其广泛的应用前景。由于目标物体遮挡、视频背景阴影、光照变化、视角变化、多尺度变化、人的衣服和外观变化等问题,使得对视频的处理与分析变得非常困难。为此,本文利用时间序列正反演构造基于张量的线性动态模型,估计模型的参数作为动作序列描述符,构造更加完备的观测矩阵。方法 首先从深度图像提取人体关节点,建立张量形式的人体骨骼正反向序列。然后利用基于张量的线性动态系统和Tucker分解学习参数元组（A_F,A_I,C）,其中C表示人体骨架信息的空间信息,A_F和A_I分别描述正向和反向时间序列的动态性。通过参数元组构造观测矩阵,一个动作就可以表示为观测矩阵的子空间,对应着格拉斯曼流形上的一点。最后通过在格拉斯曼流形上进行字典学习和稀疏编码完成动作识别。结果 实验结果表明,在MSR-Action 3D数据集上,该算法比Eigenjoints算法高13.55%,比局部切从支持向量机（LTBSVM）算法高2.79%,比基于张量的线性动态系统（tLDS）算法高1%。在UT-Kinect数据集上,该算法的行为识别率比LTBSVM算法高5.8%,比tLDS算法高1.3%。结论 通过大量实验评估,验证了基于时间序列正反演构造出来的tLDS模型很好地解决了上述问题,提高了人体动作识别率。     

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.     

On regular temporal logics with past

The IEEE standardized Property Specification Language, PSL for short, extends the well-known linear-time temporal logic LTL with so-called semi-extended regular expressions. PSL and the closely related SystemVerilog Assertions, SVA for short, are increasingly used in many phases of the hardware design cycle, from specification to verification. In this article, we extend the common core of these specification languages with past operators. We name this extension PPSL. Although all ω-regular properties are expressible in PSL, SVA, and PPSL, past operators often allow one to specify properties more naturally and concisely. In fact, we show that PPSL is exponentially more succinct than the cores of PSL and SVA. On the star-free properties, PPSL is double exponentially more succinct than LTL. Furthermore, we present a translation of PPSL into language-equivalent nondeterministic Büchi automata, which is based on novel constructions for 2-way alternating automata. The upper bound on the size of the resulting nondeterministic Büchi automata obtained by our translation is almost the same as the upper bound for the nondeterministic Büchi automata obtained from existing translations for PSL and SVA. Consequently, the satisfiability problem and the model-checking problem for PPSL fall into the same complexity classes as the corresponding problems for PSL and SVA.     

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).     

Büchi Store: an open repository of \omega -automata

We introduce Büchi Store, an open repository of Büchi automata and other types of $\omega $ -automata for model-checking practice, research, and education. The repository contains Büchi automata and their complements for common specification patterns and numerous temporal formulae. These automata are made as small as possible by various construction techniques in view of the fact that smaller automata are easier to understand and often help in speeding up the model-checking process. The repository is open, allowing the user to add automata that define new languages or are smaller than existing equivalent ones. Such a collection of Büchi automata is also useful as a benchmark for evaluating translation or complementation algorithms and as examples for studying Büchi automata and temporal logic. These apply analogously for other types of $\omega $ -automata, including deterministic Büchi and deterministic parity automata, which are also collected in the repository. In particular, the use of smaller deterministic parity automata as an intermediary helps reduce the complexity of automatic synthesis of reactive systems from temporal specifications.     

Tool support for learning Büchi automata and linear temporal logic

We introduce a graphical interactive tool, named GOAL, that can assist the user in understanding Büchi automata, linear temporal logic, and their relation. Büchi automata and linear temporal logic are closely related and have long served as fundamental building blocks of linear-time model checking. Understanding their relation is instrumental in discovering algorithmic solutions to model checking problems or simply in using those solutions, e.g., specifying a temporal property directly by an automaton rather than a temporal formula so that the property can be verified by an algorithm that operates on automata. One main function of the GOAL tool is translation of a temporal formula into an equivalent Büchi automaton that can be further manipulated visually. The user may edit the resulting automaton, attempting to optimize it, or simply run the automaton on some inputs to get a basic understanding of how it operates. GOAL includes a large number of translation algorithms, most of which support past temporal operators. With the option of viewing the intermediate steps of a translation, the user can quickly grasp how a translation algorithm works. The tool also provides various standard operations and tests on Büchi automata, in particular the equivalence test which is essential for checking if a hand-drawn automaton is correct in the sense that it is equivalent to some intended temporal formula or reference automaton. Several use cases are elaborated to show how these GOAL functions may be combined to facilitate the learning and teaching of Büchi automata and linear temporal logic. This work was partially supported by the National Science Council, Taiwan (R.O.C.) under grants NSC94-2213-E-002-089, NSC95-2221-E-002-127, NSC95-3114-P-001-001-Y02 (iCAST 2006), NSC96-3114-P-001-002-Y (iCAST 2007), and NSC97-2221-E-002-074-MY3.     

From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata

Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper, we describe a single exponential translation from limit-deterministic Büchi automata (LDBA) to DPA and show that it can be concatenated with a recent efficient translations from LTL to LDBA to yield a double exponential, ‘Safraless’ LTL-to-DPA construction. We also report on an implementation and a comparison with other LTL-to-DPA translations on several sets of formulas from the literature.

     

联锁逻辑形式化模型检验的研究

利用自动机理论模型检验算法，检验车站联锁逻辑的有色Petri网模型是否满足预期的性能。通过采用带标签的广义Büchi自动机(LGBA)构建线性时态逻辑，有效地解决了模型检验中的状态空间爆炸问题。该方法的研究增强了有色Petri网的分析和验证能力，利用该方法对车站联锁逻辑的实际问题进行了性能验证。     

A theory of ultimately periodic languages and automata with an application to time granularity

In this paper, we develop a theory of regular ω-languages that consist of ultimately periodic words only and we provide it with an automaton-based characterization. The resulting class of automata, called ultimately periodic automata (UPA), is a subclass of the class of Büchi automata and inherits some properties of automata over finite words (NFA). Taking advantage of the similarities among UPA, Büchi automata, and NFA, we devise efficient solutions to a number of basic problems for UPA, such as the inclusion, the equivalence, and the size optimization problems. The original motivation for developing a theory of ultimately periodic languages and automata was to represent and to reason about sets of time granularities in knowledge-based and database systems. In the last part of the paper, we show that UPA actually allow one to represent (possibly infinite) sets of granularities, instead of single ones, in a compact and suitable to algorithmic manipulation way. In particular, we describe an application of UPA to a concrete time granularity scenario taken from clinical medicine.