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

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

有限状态自动机的并行确定化及过程分析

本文通过对并行环境下非确定有限自动机和确定有限自动机的等价性和转换进行研究，详细分析了非确定有限自动机到确定有限自动机的并行转换方法及算法，并以实例给出了其间并行转化的过程。     

确定有限自动机最小化算法的并行处理

对有限自动机模型最小化做了深入分析,提出了一种基于可区分状态表结构的并行最小化算法,以实例详细描述了算法并行处理过程并验证其算法的可行性.     

确定型模糊多重集有限自动机的极小化

主要研究确定型模糊多重集有限自动机的状态极小化问题。给出了模糊多重集有限自动机的同余和同态概念,并利用同余和同态关系研究了确定型模糊多重集有限自动机的极小化问题。进一步从确定型模糊多重集有限自动机自身出发,构造出极小模糊多重集有限自动机,并给出了极小化的算法。     

非确定有穷自动机在盲文转码中的应用

对盲人使用的计算机交互技术进行研究是很有意义的工作。盲文字库缺少国际标准和不同公司的盲文字库不兼容造成了很多难题。将盲文用汉字点位编码表示,能摆脱盲文字库的束缚。用不确定有穷自动机描述盲文与汉字点位编码的转换过程,再用逆序拆分子集法对其确定化。经测试系统的转码正确率达到100%,从而实现盲文与机器无关,使得盲人使用计算机更方便。     

确定有穷自动机的最小化问题探讨

本文针对DFA最小化时可能遇到的各种情形,给出最小化的通用算法,并通过具体实例加以验证。此算法有利于学生对编译原理课程中DFA最小化的学习和理解,同时让学生进一步了解此知识点在其他问题求解中的应用。     

PSL构造双向交换自动机及非确定自动机的方法

PSL(property specification language)是一种用于描述并行系统的属性规约语言,包括线性时序逻辑FL(foundation language)和分支时序逻辑OBE(optional branching extension)两部分.由于OBE就是CTL(computation tree logic),并且具有时钟声明的公式很容易改写成非时钟公式,因此重点研究了非时钟FL逻辑.为便于进行模型检验,每个FL公式必须转化成为一种可验证形式,通常是自动机(非确定自动机).构造非确定自动机的过程主要是通过中间构建交换自动机来实现.详细给出了由非时钟FL构造双向交换自动机的构造规则.构造规则的核心逻辑不仅仅局限于是在LTL(linear temporal logic)基础上的正规表达式,而且全面而充分地考虑了各种FL操作算子的可能性.并且给出了将双向交换自动机转化为非确定自动机的一种方法.最后,编写了将PSL转化为上述自动机的实现工具.FL双向交换自动机的构造规则计算复杂度仅是FL公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

基于信息系统的确定有限自动机最小化算法

目前,确定有限自动机(DFA)最小化问题多侧重于理论研究,尚无太多便于实现的算法,为此,对确定有限自动机最小化方法进行了研究,提出将DFA转换为信息系统,基于等价类划分方法简化信息系统,再将简化的信息系统转换为最小化DFA;针对上述处理过程,给出一个基于分治思想的DFA最小化算法,在平均情况下该算法的时间复杂度为O(n log n),空间复杂度为O(n)。最后通过实例验证了所提算法的正确性。     

基于子集构造法的优化的NFA确定化算法

使用子集构造法对非确定有限自动机进行确定化的过程中存在大量重复计算的问题.为解决此问题,基于非确定有限自动机的特点并针对子集构造法的不足,提出了一种优化的非确定有限自动机确定化算法.首先定义了识别符的有效引出状态集概念并证明了ε-closure的并定理以保证算法的正确性,其次给出了用于避免重复计算的识别符的有效引出状态集的构造子算法和单状态集的ε-closure的求算子算法,基于这两个子算法给出了优化的非确定有限自动机确定化算法,最后将算法应用于实例,实验结果表明计算量远小于子集构造法的计算量.相比子集构造法,算法能更有效地对非确定有限自动机进行确定化.     

基于确定的有限自动机的工作流机制研究

工作流作为企业流程建模的核心技术,具有方便性、灵活性和可配置性的特点,极大的弥补了传统企业信息系统的不足。工作流引擎作为工作流重要的实现手段,是大量办公自动化系统的核心组件,其流转过程的理论研究具有重要的理论和现实意义。
　　本文提出了用确定的有限自动机来研究工作流运转过程的方法,将工作流运转中的各个步骤映射为各项状态和迁移过程,采用确定的有限自动机的观点来描绘和阐述,从而得到了工作流流转的数学模型——自动机的状态迁移图。在此基础上,可以采用自动机理论来分析和研究中工作流的流转过程,从而改善和优化工作流审批流程。     

Determinization and minimization of finite acyclic automata by incremental techniques

The determinization of a nondeterministic finite automaton (FA) is the process of generating a deterministic FA (DFA) equivalent to (sharing the same regular language of) . The minimization of is the process of generating the minimal DFA equivalent to . Classical algorithms for determinization and minimization are available in the literature for several decades. However, they operate monolithically, assuming that the FA to be either determinized or minimized is given once and for all. By contrast, we consider determinization and minimization in a dynamic context, where augments over time: after each augmentation, determinization and minimization of into is required. Using classical monolithic algorithms to solve this problem is bound to poor performance. An algorithm for incremental determinization and minimization of acyclic finite automata, called IDMA, is proposed. Despite being conceived within the narrow domain of model‐based diagnosis and monitoring of active systems, the algorithm is general‐purpose in nature. Experimental evidence indicates that IDMA is far more efficient than classical algorithms in solving incremental determinization and minimization problems. Copyright © 2015 John Wiley & Sons, Ltd.     

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.     

基于自动机理论的分布式实时调度分析工具

分布式实时系统是广泛应用在众多关键领域的一类复杂实时系统.为保证其上运行任务的实时性,传统基于最坏响应时间的调度分析方法往往包含了实际系统运行过程中无法达到的最坏情况,因此在这些情况下的分析结果过于悲观.基于自动机理论的模型检测方法的好处在于能够穷尽地搜索整个系统状态空间,得到精确的分析结果.为了利用形式化方法的优势来...     

Autowrite: A Tool for Term Rewrite Systems and Tree Automata

Autowrite is an experimental software tool written in Common Lisp Oriented System (CLOS) which handles term rewrite systems and bottom-up tree automata. A graphical interface written using McCLIM, (the free implementation of the CLIM specification) frees the user of any Lisp knowledge. Software and documentation can be found at http://dept-info.labri.u-bordeaux.fr/~idurand/autowrite. Autowrite was initially designed to check call-by-need properties of term rewrite systems. For this purpose, it implements the tree automata constructions used in [F. Jacquemard. Decidable approximations of term rewriting systems. In Proc. 7th RTA, volume 1103 of LNCS, pages 362–376, 1996; I. Durand and A. Middeldorp. Decidable call by need computations in term rewriting (extended abstract). In Proc. 14th CADE, volume 1249 of LNAI, pages 4–18, 1997; Irène Durand and Aart Middeldorp. On the complexity of deciding call-by-need. Technical Report 1196–98, LaBRI, 1998; T. Nagaya and Y. Toyama. Decidability for left-linear growing term rewriting systems. Information and Computation, 178(2):499–514, 2002] and many useful operations on terms, term rewrite systems and tree automata.     

基于时间自动机的嵌入式系统调度分析工具

为验证嵌入式实时系统开发过程中任务集的可调度性,设计并实现一种嵌入式系统调度分析工具。提出通用任务模型,建立任务与事件到达自动机和任务状态自动机的状态关系映射,利用基于模型检测的时间自动机可达性方法判定系统的可调度性。仿真实例结果表明,该工具的分析准确性较高。     

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

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

Temporal determinization of mutating finite automata: Reconstructing or restructuring

A mutating finite automaton (MFA) is a nondeterministic finite automaton (NFA) that changes its morphology over discrete time by a sequence of mutations. This results in a sequence of NFAs, the initial NFA, and one mutated NFA for each mutation. Some application domains, including model-based diagnosis of discrete-event systems in artificial intelligence and model-based testing in software engineering, require temporal determinization of MFAs. Determinizing an MFA temporally means generating a deterministic finite automaton (DFA) that is equivalent to the mutated NFA as soon as a mutation occurs. Since, in computation time, the classical Subset Construction determinization algorithm may be less than optimal when applied to MFAs, a conservative algorithm is proposed, called Subset Restructuring, which, instead of constructing the new DFA from scratch based on the mutated NFA, generates the new DFA by updating the previous DFA based on the mutation occurred. Subset Restructuring is sound and complete, thereby yielding the same DFA generated by Subset Construction. Results from massive experimentation indicate the viability of Subset Restructuring, especially so when large MFAs change by small mutations.     

Weak bisimulation for Probabilistic Timed Automata

We are interested in describing timed systems that exhibit probabilistic behaviour. To this purpose, we consider a model of Probabilistic Timed Automata and introduce a concept of weak bisimulation for these automata, together with an algorithm to decide it. The weak bisimulation relation is shown to be preserved when either time, or probability is abstracted away. As an application, we use weak bisimulation for Probabilistic Timed Automata to model and analyze a timing attack on the dining cryptographers protocol.