BACH:线性混成系统有界可达性模型检验工具

混成自动机的模型检验问题非常困难,即使是其中相对简单的一个子类--线性混成自动机,它的可达性问题仍然是不可判定的.现有的相关工具大都使用多面体计算来判定线性混成自动机状态空间的可达集,复杂度高、效率低,无法解决实际应用规模的问题.描述了一个面向线性混成系统有界可达性模型检验工具--BACH(bounded reacha...     

处理图像语言的格点自动机与格点文法

Giammarresi与Restivo在一篇综述中总结出一个关于可识别的图像语言(即2维矩形语言)REC的等价性定理.对比1维字语言的相应结果,其中还缺少关于生成文法的相应一环.提出了一种(矩形的)格点文法,正好弥补了这一缺环.而取代2维on-line tesselation自动机,引入了格点自动机的概念.一方面,它与经典的2元树型自动机更相似,另一方面,它也是格点文法与等价性定理中关于REC的其他描述方式之间的一座桥梁.同时,标准的existential monadic二阶逻辑也被一种更弱的规范框架——positive monadic分划逻辑所取代.由此导出一个新的更完整的关于REC的等价性定理.     

On the use of energy minimization for CA based analysis in elasticity

There has been recent interest in exploring alternative computational models for structural analysis that are better suited for a design environment requiring repetitive analysis. The need for such models is brought about by significant increases in computer processing speeds, realized primarily through parallel processing. To take full advantage of such parallel machines, however, the computational approach itself must be revisited from a totally different perspective; parallelization of inherently serial paradigms is subject to limitations introduced by a requirement of information coordination. The cellular automata (CA) model of decentralized computations provides one such approach which is ideally tailored for parallel computers. The proposed paper examines the applicability of the cellular automata model in problems of 2-D elasticity. The focus of the paper is in the use of a genetic algorithm based optimization process to derive the rules for local interaction required in evolving the cellular automata. Received August 28, 2000     

Conformance Tests for Real-Time Systems with Timed Automata Specifications

A method is introduced for testing the conformance of implemented real-time systems to timed automata specifications. Uppaal timed automata are transformed into testable timed transition systems (TTTSs) using a test view. Fault hypotheses and a test generation algorithm for TTTSs are defined. Results of applying the method are presented. Received October 1999 / Accepted in revised form November 2000     

On Aperiodic and Star-Free Formal Power Series in Partially Commuting Variables

Formal power series over non-commuting variables have been investigated as representations of the behavior of automata with multiplicities. Here we introduce and investigate the concepts of aperiodic and of star-free formal power series over semirings and partially commuting variables. We prove that if the semiring K is idempotent and commutative, or if K is idempotent and the variables are non-commuting, then the product of any two aperiodic series is again aperiodic. We also show that if K is idempotent and the matrix monoids over K have a Burnside property (satisfied, e.g. by the tropical semiring), then the aperiodic and the star-free series coincide. This generalizes a classical result of Schützenberger (Inf. Control 4:245–270, 1961) for aperiodic regular languages and subsumes a result of Guaiana et al. (Theor. Comput. Sci. 97:301–311, 1992) on aperiodic trace languages. This work partly supported by the DAAD-PROCOPE project Temporal and Quantitative Analysis of Distributed Systems.     

An optimal effective controller for discrete event systems

An approach to the online synthesis of an optimal effective controller for discrete event systems is presented. The optimal effective controller can achieve the prescribed (cumulative) effectiveness measure while minimizing the total cost incurred for the execution of events. This approach is constructed over a generalized control framework for automata‐based discrete event systems, which allows event enforcement in addition to the (original) event disablement/enablement as the control mechanism. The optimal effective control policy generated by this approach is proved to be the least restrictive among all the possible optimal effective control policies for the given online expansion tree of the system behavior. Copyright © 2008 John Wiley and Sons Asia Pte Ltd and Chinese Automatic Control Society     

Safe design of high-performance embedded systems in an MDE framework

In this paper, we use the UML MARTE profile to model high-performance embedded systems (HPES) in the GASPARD2 framework. We address the design correctness issue on the UML model by using the formal validation tools associated with synchronous languages, i.e., the SIGALI model checker, etc. This modeling and validation approach benefits from the advantages of UML as a standard, and from the number of validation tools built around synchronous languages. In our context, model transformations act as a bridge between UML and the chosen validation technologies. They are implemented according to a model-driven engineering approach. The modeling and validation are illustrated using the multimedia functionality of a new-generation cellular phone.     

An overview of quantum computation models: quantum automata

Quantum automata, as theoretical models of quantum computers, include quantum finite automata (QFA), quantum sequential machines (QSM), quantum pushdown automata (QPDA), quantum Turing machines (QTM), quantum cellular automata (QCA), and the others, for example, automata theory based on quantum logic (orthomodular lattice-valued automata). In this paper, we try to outline a basic progress in the research on these models, focusing on QFA, QSM, QPDA, QTM, and orthomodular lattice-valued automata. Also, other models closely relative to them are mentioned. In particular, based on the existing results in the literature, we finally address a number of problems to be studied in future.     

State Observation and Diagnosis of Discrete-Event Systems Described by Stochastic Automata

The problems ofstate observation and diagnosis are solved for discrete–eventsystems, which are described by stochastic automata. As manysystems are not observable in the sense that it is possible toreconstruct the state unambiguously, the observation problemis set up as the problem of determining the smallest possibleset of states that are compatible with the measured input andoutput sequences. The diagnostic problem is shown to be, in principle,an observation problem. Conditions for the observability anddiagnosability of stochastic automata are presented. The resultsare illustrated by examples.