模糊剩余自动机

在[0,1]格值区间上引入了模糊剩余自动机(FRFA)的概念:若一个模糊自动机(FFA)的每一个状态都定义了其接受语言的一个剩余语言,则称为模糊剩余自动机.讨论了模糊剩余自动机的一些性质以及模糊自动机的消去与饱和运算.在定义既约模糊剩余语言的基础上定义了标准模糊剩余自动机,并给出了构造方法.证明了一个模糊正则语言对应的标准FRFA即为识别这个语言的最小状态FFA,此研究为模糊自动机的状态最小化研究提供了另一种研究思路.     

可逆模糊自动机

首先提出了可逆模糊自动机的概念,研究了能被可逆模糊自动机接受的语言(简记为F(∑))的一些性质.其次给出了自由群上被可逆模糊自动机接受的模糊子集的概念,详细研究了可逆模糊语言与经典可逆语言的关系.最后,通过引入语法幺半群刻画了F(∑)的代数性质.通过这些性质可以有效的判断一个模糊语言是否能被一个可逆模糊自动机接受.     

基于互模拟的三支粒化近似

本文提出了基于互模拟的三支粒化近似,揭示了基于潜在关系的三支粒化近似和基于互似(由潜在关系诱导的最大的互模拟)的三支粒化近似之间的关系.     

模糊Rabin自动机和模糊Game自动机的等价性

自动机是理论计算机的一个重要的研究内容.模糊Rabin自动机和模糊Game自动机是经典自动机的延续,给出了模糊Rabin自动机和模糊Game自动机的相关定义,讨论各自的内在性质,并得到了二者的等价关系.这进一步丰富了模糊自动机理论.     

有限模糊树自动机的一些代数性质与相应的语言

将模糊自动机的同态、完全、容许关系等概念引入到模糊树自动机中,从代数的角度研究模糊树自动机的一些代数性质,并探讨了模糊树自动机的语言的相关问题.     

最小化基于合成模糊变换的模糊自动机

经过重新定义模糊自动机,使得模糊自动机的识别过程与一个合成模糊变换(CF变换)一致,而且得到了尊重合成模糊变换的最粗分类即为状态集的最粗等价分类这一重要结论.在对尊重合成模糊变换的最粗分类的讨论中,给出了找到尊重合成模糊变换的最粗分类的有限步算法,亦即状态集的最粗等价分类和最小化模糊自动机的算法.该算法不仅给出了最长运算时间,而且还给出可终止算法的条件,使得运算更为可行和简便.     

幺半环上几类模糊自动机的关系

给出了幺半环上非确定的模糊自动机和确定的模糊自动机及其语言的定义,证明了幺半环上三类非确定的模糊自动机间的等价性和三类确定的模糊自动机间的等价性,讨论了幺半环上三类非确定的模糊自动机和第四类非确定的模糊自动机之间的关系,以及幺半环上非确定的模糊自动机和确定的模糊自动机之间的关系.     

改进的带驻留时间隐Markov模型的前向-后向算法

对隐Maxkov模型(hidden Markov model:HMM)的状态驻留时间的概率进行了修订,给出了改进的带驻留时间隐Markov模型的结构,并在传统的隐Markov模型(traditional hidden Markov model:THMM)的基础上讨论了新模型的前向.后向变量,导出了新模型的前向-后向算法的迭代公式,同时也给出了新模型各个参数的重估公式.     

建立在模糊逻辑上的模糊元胞自动机

总结了经典元胞自动机模型理论,并在此基础上把模糊逻辑引入元胞自动机模型中.通过对模糊元胞自动机的基本原理的分析,定义了模糊元胞自动机模型.模糊元胞自动机模型可以处理模糊信息,并且使模拟与现实世界的情况更为接近.     

基于模糊互补判断矩阵的对数最小一乘法及算法程序设计

利用正互反判断矩阵与模糊互补判断矩阵的转换关系,探讨模糊互补判断矩阵的一种排序方法——对数最小一乘法,并给出这种算法的程序设计.     

Modal and guarded characterisation theorems over finite transition systems

We explore the finite model theory of the characterisation theorems for modal and guarded fragments of first-order logic over transition systems and relational structures of width two. A new construction of locally acyclic bisimilar covers provides a useful analogue of the well known tree-like unravellings that can be used for the purposes of finite model theory. Together with various other finitary bisimulation respecting model transformations, and Ehrenfeucht–Fraïssé game arguments, these covers allow us to upgrade finite approximations for full bisimulation equivalence towards approximations for elementary equivalence. These techniques are used to prove several ramifications of the van Benthem–Rosen characterisation theorem of basic modal logic for refinements of ordinary bisimulation equivalence, both in the sense of classical and of finite model theory.     

Quantale与互模拟的进程语义

以特定的观察为生成元构造了互模拟quantaleQ_B,而将进程作为此quantale上的模的组成成分,由此给出了互模拟的三个完备性准则,回答了AbrasmkyS与VickersS．提出的公开问题（1993）,完备了他们利用quantale统一处理进程语义的方法．     

Bisimulations for fuzzy automata

Bisimulations have been widely used in many areas of computer science to model equivalence between various systems, and to reduce the number of states of these systems, whereas uniform fuzzy relations have recently been introduced as a means to model the fuzzy equivalence between elements of two possible different sets. Here we use the conjunction of these two concepts as a powerful tool in the study of equivalence between fuzzy automata. We prove that a uniform fuzzy relation between fuzzy automata A and B is a forward bisimulation if and only if its kernel and co-kernel are forward bisimulation fuzzy equivalence relations on A and B and there is a special isomorphism between factor fuzzy automata with respect to these fuzzy equivalence relations. As a consequence we get that fuzzy automata A and B are UFB-equivalent, i.e., there is a uniform forward bisimulation between them, if and only if there is a special isomorphism between the factor fuzzy automata of A and B with respect to their greatest forward bisimulation fuzzy equivalence relations. This result reduces the problem of testing UFB-equivalence to the problem of testing isomorphism of fuzzy automata, which is closely related to the well-known graph isomorphism problem. We prove some similar results for backward-forward bisimulations, and we point to fundamental differences. Because of the duality with the studied concepts, backward and forward-backward bisimulations are not considered separately. Finally, we give a comprehensive overview of various concepts on deterministic, nondeterministic, fuzzy, and weighted automata, which are related to bisimulations.     

Modal characterisation theorems over special classes of frames

We investigate model theoretic characterisations of the expressive power of modal logics in terms of bisimulation invariance. The paradigmatic result of this kind is van Benthem’s theorem, which says that a first-order formula is invariant under bisimulation if, and only if, it is equivalent to a formula of basic modal logic. The present investigation primarily concerns ramifications for specific classes of structures. We study in particular model classes defined through conditions on the underlying frames, with a focus on frame classes that play a major role in modal correspondence theory and often correspond to typical application domains of modal logics. Classical model theoretic arguments do not apply to many of the most interesting classes-for instance, rooted frames, finite rooted frames, finite transitive frames, well-founded transitive frames, finite equivalence frames-as these are not elementary. Instead we develop and extend the game-based analysis (first-order Ehrenfeucht-Fraïssé versus bisimulation games) over such classes and provide bisimulation preserving model constructions within these classes. Over most of the classes considered, we obtain finite model theory analogues of the classically expected characterisations, with new proofs also for the classical setting. The class of transitive frames is a notable exception, with a marked difference between the classical and the finite model theory of bisimulation invariant first-order properties. Over the class of all finite transitive frames in particular, we find that monadic second-order logic is no more expressive than first-order as far as bisimulation invariant properties are concerned — though both are more expressive here than basic modal logic. We obtain ramifications of the de Jongh-Sambin theorem and a new and specific analogue of the Janin-Walukiewicz characterisation of bisimulation invariant monadic second-order for finite transitive frames.     

Bounded variable logics: two, three, and more

Consider the bounded variable logics (with k variable symbols), and (with k variables in the presence of counting quantifiers ). These fragments of infinitary logic are well known to provide an adequate logical framework for some important issues in finite model theory. This paper deals with a translation that associates equivalence of structures in the k-variable fragments with bisimulation equivalence between derived structures. Apart from a uniform and intuitively appealing treatment of these equivalences, this approach relates some interesting issues for the case of an arbitrary number of variables to the case of just three variables. Invertibility of the invariants for , in particular, would imply a positive answer to the tempting conjecture that fixed-point logic with counting captures Ptime . Received July 13, 1996     

On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations

We take the well-known intuitionistic modal logic of Fischer Servi with semantics in bi-relational Kripke frames, and give the natural extension to topological Kripke frames. Fischer Servi’s two interaction conditions relating the intuitionistic pre-order (or partial-order) with the modal accessibility relation generalize to the requirement that the relation and its inverse be lower semi-continuous with respect to the topology. We then investigate the notion of topological bisimulation relations between topological Kripke frames, as introduced by Aiello and van Benthem, and show that their topology-preserving conditions are equivalent to the properties that the inverse relation and the relation are lower semi-continuous with respect to the topologies on the two models. The first main result is that this notion of topological bisimulation yields semantic preservation w.r.t. topological Kripke models for both intuitionistic tense logics, and for their classical companion multi-modal logics in the setting of the Gödel translation. After giving canonical topological Kripke models for the Hilbert-style axiomatizations of the Fischer Servi logic and its classical companion logic, we use the canonical model in a second main result to characterize a Hennessy–Milner class of topological models between any pair of which there is a maximal topological bisimulation that preserve the intuitionistic semantics.     

Program derivation with verified transformations — a case study

A program development methodology based on verified program transformations is described and illustrated through derivations of a high level bisimulation algorithm and an improved minimum-state DFA algorithm. Certain doubts that were raised about the correctness of an initial paper-and-pencil derivation of the DFA minimization algorithm were laid to rest by machine-checked formal proofs of the most difficult derivational steps. Although the protracted labor involved in designing and checking these proofs was almost overwhelming, the expense was somewhat offset by a successful reuse of major portions of these proofs. In particular, the DFA minimization algorithm is obtained by specializing and then extending the last step in the derivation of the high level bisimulation algorithm. Our experience suggests that a major focus of future research should be aimed towards improving the technology of machine checkable proofs — their construction, presentation, and reuse. This paper demonstrates the importance of such a technology to the verification of programs and program transformations. We believe that the utility of transformational systems to program development will ultimately rest on a practical program correctness technology. © 1996 John Wiley & Sons, Inc.     

Bisimulations and bisimulation games between Verbrugge models

Interpretability logic is a modal formalization of relative interpretability between first-order arithmetical theories. Verbrugge semantics is a generalization of Veltman semantics, the basic semantics for interpretability logic. Bisimulation is the basic equivalence between models for modal logic. We study various notions of bisimulation between Verbrugge models and develop a new one, which we call w-bisimulation. We show that the new notion, while keeping the basic property that bisimilarity implies modal equivalence, is weak enough to allow the converse to hold in the finitary case. To do this, we develop and use an appropriate notion of bisimulation games between Verbrugge models.     

Existence theorems of solution to variational inequality problems

This paper introduces a new concept of exceptional family for variational inequality problems with a general convex constrained set. By using this new concept, the authors establish a general sufficient condition for the existence of a solution to the problem. This condition is weaker than many known solution conditions and it is also necessary for pseudomonotone variational inequalities. Suffi-cient solution conditions for a class of nonlinear complementarity problems with Po mappings are also obtained.