概率有限状态自动机的代数性质

利用矩阵、同态、同构、同余等代数工具研究概率有限状态自动机的代数性质.首先定义了输入集上两个字符串同余的概念,并利用概率转移矩阵给出2个字符串同余的一些等价刻画.进而提出概率有限状态自动机同态和同构的概念,并给出了概率有限状态自动机同态定理.证明了2个概率有限状态自动机同构的充要条件是它们的概率转移矩阵可以通过第1种行列初等变换相互转化;同时提出了2个概率有限状态自动机积与和的概念,并得到了积自动机、和自动机的同态关系.最后将模糊自动机中交换的概念引入到概率有限状态自动机中,并利用概率转移矩阵给出了此类自动机交换的一些等价刻画以及和自动机、积自动机交换的充要条件.     

实时系统的模型检验中针对共享变量的优化技术

实时系统可以使用由多个并发的时间自动机组成的时间自动机网络来建模。网络中的时间自动机通过共享变量和/或信道交互。带有不同共享变量取值的自动机网络的状态是截然不同的。因此,共享变量也是引起状态空间爆炸问题的原因之一。本文提出了在不同共享变量取值之间的兼容性关系的概念。使用这种兼容性关系,时间自动机网络的可达性分析算法就可以减少需要遍历的状态的个数。本文给出了检测符号化状态中共享变量的取值所能兼容的其它取值的算法以及进一步进行这种兼容性关系检测的增强算法。最后还给出了使用了这两种算法进行优化之后的可迭性分析算法。实验结果显示经优化的可达性分析算法的空间效率得到了显著的提高。     

模糊有限自动机的最小化算法优化

现有的模糊自动机最小化算法没有涉及到对模糊自动机状态的隶属度迁移和变化的讨论,优化的模糊自动机最小化算法弥补了这类算法的不足之处。该算法将模糊有限自动机首先转化为单个初始状态的模糊自动机,然后再将转化后的模糊自动机化简为最小模糊自动机,算法在转化过程中单独讨论了模糊自动机状态隶属度的转化方式,使得算法更加严谨和简化。     

基于自动机的分析与综合因素神经网络的自动实现方法

本文讨论了因素神经网络与自动机的关系及分析与综合因素神经网络的自动机算法。刻画了因素神经网络的状态集合及正则模糊文法的生成式链，给出了自动机算法的形式化，使对神经网络的分析与综合可在计算机上得以自动实现。     

量子自动机的交换性

定义了量子自动机及广义量子自动机的交换性,并提出了（广义）量子自动机所识别语言的交换性。利用半群及矩阵研究（广义）量子自动机的交换性,得出了（广义）量子自动机交换性的几个等价刻画。研究了（广义）量子自动机的交换性与其所识别语言的交换性的关系,证明了交换的（广义）量子自动机所识别的语言也是交换的。此外,讨论了（广义）量子自动机的广义直积、全直积、限制直积、级联积和圈积等积的交换性,得出了一些积的交换性的充分条件和必要条件。     

离散事件系统的无死锁模块化状态反馈控制

本文讨论离散事件系统的无死锁模块化状态反馈问题。首先我们定义自动机的交与并运算，然后通过引入自动机对的Ｄ－不变关系，我们证明当控制目标是两个谓词的交时，模块化状态反馈控制器是无死锁的充要条件是各子控制器是无死锁的且相应的控制器满足Ｄ－不变关系。我们证明了一个给定的自动机对于另一自动机的Ｄ－不变子自动机类有最大元存大，并由此给出一个综合算法。     

基于自动机的微博在线突发话题检测算法

提出一种基于状态自动机的突发特征检测算法,针对微博数据长度小,语言不规范,噪声大,数据量大的特点,优化预处理过程和状态自动机模型参数;提出一种突发话题聚类算法,对特征词的词频向量表示进行改进,并引入基于词激活力(WAF)的词法特征,使得聚类效果更加准确,得到的突发话题可读性更强.最后通过实验方法验证了算法的可行性.     

基于时态逻辑的UML交互模型检测研究

该文详细介绍了统一建模语言和模型检测技术,在此基础上,该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。     

采用动作时序逻辑的Web服务组合方法

基于有限状态自动机理论,将Web服务建模成一个有限状态自动机。针对网络服务描述语言(WSDL)在服务行为描述方面的缺陷对其进行扩展,提出了从扩展的WSDL到动作时序逻辑(TLA)语言的转换算法,从而可以用TLA对服务行为进行形式化描述和规范,为描述Web服务提供了一个新的方法。讨论了在动作时序逻辑中,服务组合时各组件服务的有限状态自动机的组合方式,以及伴随着服务组合,单个服务的TLA规范如何组合以形成复合服务的TLA规范的问题,并在此基础上,提出了实现TLA规范正确组合的算法思想。     

一类格值自动机的极小化

给出了格值自动机的同余和同态,从代数角度出发详细研究了同余和同态关系的代数性质,揭示了格值自动机的代数性质和取值格半群的紧密联系,利用同余和同态关系最终研究了格值自动机的极小化问题,在正则同余下给出了可在有限步实现具有模糊初始状态和特殊模糊终状态的自动机极小化的算法。     

Hardness of preorder checking for basic formalisms

We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence, even if the flat system is assumed to be fixed.     

Backward and forward bisimulation minimization of tree automata

We improve on an existing [P.A. Abdulla, J. Högberg, L. Kaati, Bisimulation minimization of tree automata, International Journal of Foundations of Computer Science 18(4) (2007) 699–713] bisimulation minimization algorithm for finite-state tree automata by introducing backward and forward bisimulation and developing minimization algorithms for them. Minimization via forward bisimulation is also effective on deterministic tree automata, faster than the previous algorithm, and yields the minimal equivalent deterministic tree automaton. Minimization via backward bisimulation generalizes the previous algorithm and can yield smaller automata but is just as fast. We demonstrate implementations of these algorithms on a typical task in natural language processing.     

Intuitionistic general fuzzy automata

In this paper, by considering the notions of general fuzzy automata, admissible relation, admissible partition and intuitionistic fuzzy set based on the Atanassov (Fuzzy Sets Syst 20(1):87–96, 1986), we define the concepts intuitionistic general fuzzy automaton (IGFA), max–min intuitionistic general fuzzy automaton, admissible relation for the IGFA, admissible partition for the IGFA, quotient IGFA and language for an IGFA. In particular, a connection between the admissible partition and the quotient IGFA is presented and it is shown that any quotient of a given IGFA and the IGFA itself has the same language. Also, using the above notions, some related theorems are proved and, finally, some examples are given to clarify these new notions.     

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公式长度的线性表达式,验证了构造规则的正确性.在此基础上,证明了双向交换自动机与其转化的等价的非确定自动机接受的语言相同.上述工作对解决复杂并行系统建模和模型验证问题具有重要的理论意义和应用价值.     

Bisimulation, the Supervisory Control Problem and Strong Model Matching for Finite State Machines

A fundamental relationship between the controllability of a language with respect to another language and a set of uncontrollable events in the Supervisory Control Theory initiated by (Ramadge and Wonham, 1989) and bisimulation of automata models is derived. The theoretical results relating bisimulation to controllability support an efficient solution to the Basic Supervisory Control Problem. Using (Fernandez, 1990) generalization of the partition refinement algorithm of (Paige and Tarjan, 1987), it is possible to find a partition which represents the supremal controllable sublanguage of an automaton with respect to the language of another automaton and a set of events in a worst-case running time of O( m log(n)), where m is the number of transitions and n is the number of states. Utilizing the bisimulation property of language controllability and derived relationships between automata languages and input/output finite-state machine behaviors, a precise relationship is formally derived between Supervisory Control Theory and the system-theoretic problem posed by (DiBenedetto et al., 1994) called Strong Input/Output FSM Model Matching. Specifically, it is proven that in deterministic settings instances of each problem can be mapped to the other framework and solved.     

Exploiting symmetry in the synthesis of supervisors for discreteevent systems

We investigate a method to exploit the symmetry inherent to many discrete-event systems in order to reduce the computational complexity of the supervisory control problem (SCP). We characterize symmetry using notions of group theory and derive conditions under which there exists a quotient (reduced) automaton representation for a language with, in general, a much smaller state space than the original minimal (in number of states) automaton representation for the language. We then propose an algorithm to synthesize a solution to the SCP which is similar to the classical one, but performed on reduced automata. Special attention is given to the particular case of systems whose models contain similar components. The approach is illustrated by an example of control of a small production line     

Resolution approach to testing compatibility of interacting automata

Conclusion The notion of compatibility of automata was proposed in [1] for formalization of requirements that must be met by interacting partial automata. Testing the compatibility of automata is of essential importance for the design of systems that interact with the environment, especially when we use declarative specificatio of the system to be designed. Under the assumptions of this article for the automaton that models the environment, partiality of the specified automaton is a source of possible incompatibility with the environment. When declarative specification is used, we can never decide in advance if the specified automaton is partial or not. Moreover, even a specification thata priori describes a completely defined automaton may be altered by the actions of the designer in the process of design (especially if these actions are incorrect) so that the specified automaton becomes partial. Therefore the initial specification, and each successive specification produced by human intervention in the design process, must be tested for compatibility with the environment. In the methodology of verification design of automata, compatibility testing is used to solve two problems: a) generating the specification of the class of all automata that satisfy the initial specification and are compatible with the specification of the environment; b) testing for correctness the designer's decisions that alter the current specification of the automaton being designed. The results of this article have led to the development of an efficient resolution procedure for testing the compatibility of automaton specification with the specification of the environment. this procedure has been implemented in the system for verification design of automata from their logical specifications. The efficiency of the developed procedure is based on the results of compatibility analysis of automata from [1] and on the restricted resolution strategy whose completeness and correctness have been proved in [2]. Translated from Kibernetika i Sistemnyi Analiz, No. 6, pp. 36–50, November–December, 1994.     

Reversible pushdown automata

Reversible pushdown automata are deterministic pushdown automata that are also backward deterministic. Therefore, they have the property that any configuration occurring in any computation has exactly one predecessor. In this paper, the computational capacity of reversible computations in pushdown automata is investigated and turns out to lie properly in between the regular and deterministic context-free languages. Furthermore, it is shown that a deterministic context-free language cannot be accepted reversibly if more than realtime is necessary for acceptance. Closure properties as well as decidability questions for reversible pushdown automata are studied. Finally, we show that the problem to decide whether a given nondeterministic or deterministic pushdown automaton is reversible is P-complete, whereas it is undecidable whether the language accepted by a given nondeterministic pushdown automaton is reversible.     

软件动态正确性的形式化描述

软件正确性是一个逐渐改进的过程.通过不断地修改,软件越来越接近于正确.同时软件的执行依赖于环境.为了刻画软件的动态正确性并考虑环境的因素,以参数化互模拟为基础,利用极限的观点,建立软件动态正确性的形式化描述.首先建立参数化互模拟的无限演化理论,给出参数化极限互模拟的定义,并给出几个特殊的参数化极限互模拟实例.其次,建立参数化互模拟极限,给出参数化互模拟极限的规约刻画. 最后,证明参数化互模拟极限的唯一性、与参数化互模拟的相容性等代数性质.