Model checker aided design of a controller for a wafer scanner

For a case-study of a wafer scanner from the semiconductor industry it is shown how model checking techniques can be used to compute (1) a simple yet optimal deadlock avoidance policy, and (2) an infinite schedule that optimizes throughput. in the absence of errors. Deadlock avoidance is studied based on a simple finite state model using Smv, and for throughput analysis a more detailed timed automaton model has been constructed and analyzed using the Uppaal tool. The Smv and Uppaal models are formally related through the notion of a stuttering bisimulation. The results were obtained within 2 weeks, which confirms once more that model checking techniques may help to improve the design process of realistic, industrial systems. Methodologically, the case study is interesting since two models were used to obtain results that could not have been obtained using only a single model. Supported by the European Community Project IST-2001-35304 (Ametist), http://ametist.cs.utwente.nl/.     

A hybrid PC/PLC architecture for manufacturing-system control—theory and implementation

This paper presents a novel and generic PC/PLC-based software/hardware architecture for the control of flexible manufacturing workcells. The proposed implementation methodology is based on the utilization of any one of the available formal discrete-event-system control theories in conjunction with state-of-the-art industrial programmable-logic controllers (PLCs). The methodology has been illustrated to be a viable technique through its actual implementation in our laboratory using a robotic-workcell testbed. The specific control theory used is a combination of Extended Moore Automata and Ramadge-Wonham Automata that has been developed by our research group. The modular control software architecture has been developed for MS-Windows environments (running on one PC interfaced to the PLCs) and allows the use of different formal control theories as well as different commercial PLC hardware. The effective graphical user interface provides a transparent programming environment, where users are not expected to have a full knowledge of the formal control theory used.     

模糊自动机在电磁波识别中的应用

研制了一个模糊处理和神经网络相结合的自动机,使用模糊技术从未处理的电磁信号波纹图像中处理模糊几何特征属性,进行波纹分类与识别。当使用模糊自动机(FA)进行识别紊乱波纹时,这些模糊几何特征是最好的。而对这些模糊几何特征的辨识,使用FA是很好的。     

Cellular automata model of gravity-driven granular flows

A cellular automata model is used to simulate a variety of granular chute flows. The model is tested against several case studies: flow down a chute, flow past an obstacle, chute flow in which complex, counter-rotating vortices result in streamwise surface stripes and flow near a boundary. The model successfully reproduces experimental observations in all of these cases. These results lead us to propose that simple, rule-based, models such as this can improve our detailed understanding of dynamics and flow within an opaque granular bed.     

XML schema, tree logic and sheaves automata

XML documents may be roughly described as unranked, ordered trees and it is therefore natural to use tree automata to process or validate them. This idea has already been successfully applied in the context of Document Type Definition (DTD), the simplest standard for defining document validity, but additional work is needed to take into account XML Schema, a more advanced standard, for which regular tree automata are not satisfactory. In this paper, we introduce Sheaves Logic (SL), a new tree logic that extends the syntax of the – recursion-free fragment of – W3C XML Schema Definition Language (WXS). Then, we define a new class of automata for unranked trees that provides decision procedures for the basic questions about SL: model-checking; satisfiability; entailment. The same class of automata is also used to answer basic questions about WXS, including recursive schemas: decidability of type-checking documents; testing the emptiness of schemas; testing that a schema subsumes another one.This work was partially supported by the French government research grant ACI TRALALA and by IST Global Computing Profundis.     

凸轮逆序测量方法

目前各杂志所发表的关于凸轮测量的文章，所讨论的均是凸轮的顺序测量方法，有关凸轮的逆序测量(反求工程)方法，尚未见于文字。本文将对凸轮的逆序测量方法进行探讨。     

Cryptanalysis of an involutional block cipher using cellular automata

In 2006, an involutional block cipher using cellular automata was proposed. A self-invertible CA-based structure allows for an efficient hardware implementation. This paper analyzes the insecurity of the cipher due to its conjugate property. The results of this study will make it possible to construct a decryption process without knowledge of the secret key.     

凸轮机构推程、回程运动角的最佳匹配及其求解方法

在推程、回程运动角之和 Φ0 +Φ′0 =C(定值 )的情况下 ,必存在某一对推程、回程运动角的最佳匹配 Opti-m um{ Φ0 ,Φ′0 } ;当选用该最佳匹配时 ,对心式直动从动杆盘形凸轮基圆半径 r0 取得最小值 r0 min。本文在揭示出上述事实的基础上 ,研究解决了当选取最佳匹配 Optim um{ Φ0 ,Φ′0 }时 ,按许用压力角 [α]条件求解对心式直动从动杆盘形凸轮基圆半径最小值 r0 min的解析法。     

由有穷自动机构造正则表达式的新算法

本文借助图论的理论，通过识别回路和不包含回路的由起始状态到终止状态的路径的方法，提出一种构造给定有穷自动机对应的正则表达式的新算法，并给出具体实例。     

一种非限制性的手写数字的识别方法

本文从语义，句法模式识别观点，提出一种基于模型指导的有限状态属性自动机，进行特征抽取。对每一种典型的畸变模型设计一个有限状态属性文法及其相应的属性自动机，采用自下而上和自上而下相结合的控制策略，并在低层次引入知识指导，减少了工作量和不确定性。基于上述方法实现的非限制性手写数字识别系统，经过对１１００个非限制性手写数字样本的测试，平均识别率达９５．２％，拒识率为４．６％，误识率为０．２％。