基于等价关系的有穷自动机最小化方法

主要介绍了有穷自动机的基础知识,研究了有穷自动机的等价性,并在确定型有穷自动机的状态集上引入等价关系,给出了自动机的最小化过程。利用等价归并算法,可以将某一给定的确定型有穷自动机状态集上的等价状态归并掉,生成与其等价的最小化的确定型有穷自动机。     

一类交替的ω—有穷自动机和确定的ω—有穷自动机识别能力…

本文提出了一类交替的ω－有穷自动机，即所有状态都是万能的交替的ω－有穷自动机，并采用了构造的方法证明了ω－ＵＡＦＡ和确定的ω－有穷自动机在四种接受条件下接受的ω－语言的等价性。     

加权有穷自动机的代数性质

在加权有穷自动机理论基础上,利用强同态的概念,证明两个加权有穷自动机在计算能力上是等价的,并在加权有穷自动机的状态集上建立一种等价关系,得到加权有穷自动机的商自动机,证明加权有穷自动机与其商自动机在计算能力上也是等价的。并通过引入加权有穷自动机的可交换性、分离性、(强)连通性及层的概念,讨论在(强)同态的条件下,两个加权有限状态机之间的可交换性、分离性、(强)连通性及层的关系。关键词：     

一类交替的ω－有穷自动机和确定的ω－有穷自动机识别能力的等价性

本文提出了一类交替的ω－有穷自动机，即所有状态都是万能的交替的ω－有穷自动机（记为ω－ＵＡＦＡ），并采用了构造的方法证明了ω－ＵＡＦＡ和确定的ω－有穷自动机在四种接受条件下接受的ω－语言的等价性。     

几类带空转移的n元伪加权自动机的关系

引入了n元伪加权有穷自动机——带有n个有限字符集的伪加权有穷自动机、分明型n元伪加权有穷自动机和确定型n元伪加权有穷自动机的概念。根据状态转移函数在每个字符集上是否带空转移, 将以上自动机分为4类:带r-型空转移的n元伪加权有穷自动机和带空转移的n元伪加权有穷自动机和带r-型空转移的分明型n元伪加权有穷自动机和带空转移的分明型n元伪加权有穷自动机。给出了以上自动机所识别语言的定义并探究了它们之间的关系,讨论了状态转移函数在每个字符集上是否带空转移对其接受语言的影响。     

基于有穷自动机的路径覆盖测试方法①

软件测试是当前软件生成重要的研究课题。从源程序流程图开始,提出了基于自动机的路径覆盖算法,该算法将源程序通过转换规则构造成与之等价的有穷自动机,应用自动机的特性处理有穷自动机中回边,并通过有限自动机的覆盖路径算法实现路径覆盖测试路径的选择。此方法实现路径覆盖的目标,与其它路径覆盖算法相比,覆盖路径生成数少。     

模糊识别器与有穷自动机的等价性

针对模糊识别器与有穷自动机的关系,证明了当输入字母表相同时,任给一个模糊识别器,必然存在一个有穷自动机,使得模糊识别器的行为与有穷自动机所接受的语言相同;反之,任给一个有穷自动机,必然存在一个模糊识别器,使得有穷自动机所接受的语言与模糊识别器的行为相同,从而得出它们之间的等价性。     

论有穷状态验证方法的局限性

程序有穷状态验证方法是介于程序验证和程序测试之间的一种方法，一方面它如同程序验证一样可以证明某程序具有某些要求的性质，或找出反例证明该程序不具有所要求的性质。另一方面它又不像程序验证那样复杂，要求验证人员具有较高的形式化推理的专业理论和数学水平。但是，现有的有穷状态验证方法有很大的局限性，它要求所论证的性质是有穷自动机所接受的事件序列的集合，或等价地说该性质能表示成为正则表达式。众所周知，有穷自动机所能接受的语言类，按Chomsky字的集合的分类是很小的类。本文讨论了这种局限性，井尝试突破只能使用有穷自动机的限制，提出了一种新的验证方法——有穷路径验证法。在这种方法中，所论证的性质表示可以推广到使用任何一类自动机。作为代价，描写系统的模型限制是无环的。对于有环的描写系统的模型，本文提出了一种称之为“有穷路径测试”的方法。同一般的程序测试一样，用这种方法通过测试不能正面地验证程序的正确性，可是如果通不过测试，则能帮你发现反例，找出程序的错误。与一般的程序测试不同的是这里的测试是相对于模型的路径，而不执行实际的程序。     

基于紧凑型有穷自动机模型的告警相关处理

在网络管理领域,告警相关（Alarm Correlation)是取代简单告警过滤机构的一种全新故障管理策略。通过在非确定型有穷自动机在(ndfa)的定义中引入状态基(State Cardinality)的概念,本文首先给出紧凑型有穷自动机（cfa）的定义,然后提出了基于紧凑型有穷自动机的告警相关处理模型并进行了详尽的描述。在一个电信管理网（TMN）的故障管理子系统中应用该模型对大量的告警信息在时间上和空间上进行告警相关处理。仿真结果表明,基于紧凑型有穷自动机的告警相关处理模型的算法实现具备简单、高效、实用和实时的特点,尤其对并发故障具有较强的相关处理能力。     

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

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

Equivalence of infinite behavior of finite automata

Given a finite automaton, its infinite behavior is defined by Büchi (1962), Eilenberg (1974) and McNaughton (1966) as the set of all infinite sequences of letters which label paths passing infinitely many times through a given subset of states. Two finite automata are said to be equivalent when their infinite behaviors are equal.In this paper we give a necessary and sufficient condition of equivalence, which uses considerations over finite behaviors only. An algorithm for the general case (deterministic or not) is given; its time and space complexity is better than any other existent method.     

Controlled finite automata

This paper discusses finite automata regulated by control languages over their states and transition rules. It proves that under both regulations, regular-controlled finite automata and context-free-controlled finite automata characterize the family of regular languages and the family of context-free languages, respectively. It also establishes conditions under which any state-controlled finite automaton can be turned into an equivalent transition-controlled finite automaton and vice versa. The paper also demonstrates a close relation between these automata and programmed grammars. Indeed, it proves that finite automata controlled by languages generated by propagating programmed grammars with appearance checking are computationally complete. In fact, it demonstrates that this computational completeness holds even in terms of these automata with a reduced number of states.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

Decomposing a kind of weakly invertible finite automata with delay 2

Some properties of a finite automaton composed of two weakly invertible finite automata with delay 1 are given,where each of those two automata has the output set of each state with the same size.And for a weakly invertible finite automaton M with delay 2 satisfying the properties mentioned in this paper,two weakly invertible finite automata with delay 1 are constructed such that M is equivalent to a sub-finite-automaton of the composition of those two.So a method to decompose this a kind of weakly invertible finite automate with delay 2 is presented.     

DISCRETE-TIME SYSTEMS THAT ADMIT FINITELY MANY CAUSAL STATE-REPRESENTATIONS

In this paper, relationship between causal discrete-time systems and the number of their causal state-representations is studied using the metric structure defined on the input and output sets of the systems, which enables us to introduce some topological notions to the investigation. For any given causal discrete-time system, an equivalence relation is defined on the input set, where any two inputs are equated if they equally distinguish all possible causal states of the system, and the quotient set of the input set with respect to the equivalence relation is studied in detail. The main results include: A discrete-time system admits essentially only a finite number of causal state-representations if and only if it is finitely observable. As an application, an algorithm to decide if a finite-state automaton has only finitely many automata having the same behavior as that of the original automaton is obtained.     

An improved algorithm for determinization of weighted and fuzzy automata

For a given weighted finite automaton over a strong bimonoid we construct its reduced Nerode automaton, which is crisp-deterministic and equivalent to the original weighted automaton with respect to the initial algebra semantics. We show that the reduced Nerode automaton is even smaller than the Nerode automaton, which was previously used in determinization related to this semantics. We determine necessary and sufficient conditions under which the reduced Nerode automaton is finite and provide an efficient algorithm which computes the reduced Nerode automaton whenever it is finite. In determinization of weighted finite automata over semirings and fuzzy finite automata over lattice-ordered monoids this algorithm gives smaller crisp-deterministic automata than any other known determinization algorithm.     

一类并发实时系统的自动验证

一个被广泛用于验证实时系统的方法是根据被验证的实时性质,使用适当的双向模拟等价关系使无限的状态空间转化为有限的状态等价类空间.算法只需要在这个有限的等价类空间里搜索就可以得到正确答案.但是,这个等价类空间的规模一般随着系统规模的增大而产生爆炸性的增长,以至于在很多情况下,穷尽搜索这个空间是不现实的.该文引入了一个等价关系来验证一个由多个实时自动机通过共享变量组成的并发系统是否满足一个线性时段特性.同时,还引入了格局之间的兼容关系来避免对状态等价类空间的穷尽搜索.基于这两个关系,文章提出了一个算法来验证是否一个实时自动机网满足一个线性时段特性.实例研究显示,此算法在某些情况下比其他一些工具有更好的时间和空间效率.     

Input-trees of finite automata and application to cryptanalysis

In this paper,Weights of output set and of input set for finite automata are discussed.For a weakly invertible finite automaton,we prove that for states with minimal output weight,the distruibution of input sets is uniform.Then for a kind of compound finite automata,we give weights of output set and of input set explicitly,and a characterization of their input-trees.For finite automaton public key cryptosystems,of which automata in public keys belong to such a kind of compound finite automata,we evaluate search amounts of exhaust search algorithms in average case and in worse case for both encryption and signature,and success ful probabilities of stochastic search algorithms for both encryption and signature.In addition,a result on mutual invertibility of inite automata is also given.     

自动验证并发实时系统的线性时段性质

介绍了一个就线性时段性验证实时系统正确性的工具的设计思想以及相关算法,使用时间自动机作为产时系统的描述模型,同时,为了便珩描述并发实时系统,使用带共享变量和通道的时间自动机网作为模型描述并发实时系统,在检验时间自动机网时,用户可以使用工具提供的合成程序将其合并为一个时间自动机然后进行检验,由于时间自动机的状态空间是无究的,通过引入整数状态和状态等价关系的概念,将整个状态0空间划分为有限的状态等价类空间,模型检验过程只需要通过对等价类空间的搜索就可以完成,但往往等价类空间的规模很大,超出了现在计算机的处理能力,原始搜索算法仅仅在理论上是可知地的,为了增工具的使用性,工具中使用的算法运用了一些优化技术来避免对等价类空间的穷尽搜索,使得工具在使用时具有比较好的时间和空间效率。     

Complexity of control on finite automata

We consider control questions for finite automata viewed as input/output systems. In particular, we find estimates of the minimal number of states of an automaton able to control a given automaton. We prove that, on average, feedback closed-loop control automata do not have fewer states than open-loop control automata when the control objective is to steer the controlled automaton to a target state. We compare our approach to other ways of formalizing of formalizing analogous control objectives.