广义可能性互模拟及其逻辑刻画

首先,给出了基于广义可能性测度的计算树逻辑的扩展GPoCTL*、计算树逻辑的约简GPoCTL-以及带回报的计算树逻辑GPoRCTL的语构和语义。在经典互模拟和广义可能性测度的基础上讨论了广义可能性互模拟及其相关性质。最后证明了GPoCTL、GPoCTL*和GPoCTL-公式与互模拟状态之间的等价关系。     

自动机,逻辑与博弈

讨论了特定的自动机、自动机的识别能力、逻辑的表达能力和博弈思想的关系。使用博弈思想可以比较容易地证明一元二阶逻辑(S1S和S2S)的可决定性。主要考虑线性时间(linear time)与分支时间(branch time)两种情况，通过这些逻辑与别的时态逻辑的表达能力的等价性可以证明其它逻辑也具有决定性，可以设计相应的自动机去解决模型检查(Model Checking)问题。     

连续时间Markov决策过程互模拟等价及逻辑保持

模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.     

基于认知反映的信念逻辑

Quine[9]提出了一类有关信念模态的难题,比如Cicero难题,这些难题的解读对模态逻辑语义具有重要的意义.目前的一阶模态逻辑普遍给予Quine难题以de re/de dicto解读.本文指出de re/de dicto解读存在缺陷,并且认为为了解读Quine难题,需要在一阶模态逻辑的模型中引入一个认知反映关系.在此观念下,本文提出了一个新的一阶模态逻辑系统--基于认知反映的信念逻辑.     

基于可能性测度的计算树逻辑CTL*与可能性互模拟

提出了基于可能性测度的计算树逻辑CTL*(PoCTL*)的概念。给出了在可能的Kripke结构中可能性互模拟的定义并对其性质进行了详细的探讨。对商可能性Kripke结构及其相关构造进行了特别的研究。     

搜索算法的逻辑分析*

搜索算法的初始空间、搜索策略、搜索过程可以用一阶语言描述,搜索算法的逻辑性质由初始状态空间确定.这意味着描述搜索过程的逻辑具有紧致性,初始状态的初等类具有有限封闭性.     

绿色评价模型的互模拟等价及逻辑保持

绿色计算中,复杂系统的绿色评价是一个重要的研究课题,其核心任务是判断运行时时间、空间资源消耗是否满足环境约束或限定.设计时,采用模型检测技术,自动、完备、高效地进行绿色评价,是一种新颖且有效的解决方案,但可能出现的状态爆炸问题将影响评价成败或效率.引入随机决策过程作为绿色评价模型;用时态逻辑刻画包含行为正确性及时间、空间资源约束的绿色评价指标;定义不确定语义理解下评价模型状态的互模拟等价规则,给出互模拟商的构造方法以及商模型调度,并比较等价语义下的行为机理;运用结构化归纳法证明互模拟等价保持评价结论.分析表明,互模拟等价可用作状态约简手段,为基于模型的绿色评价提供理论支撑和技术手段.     

归纳逻辑程序设计综述

归纳逻辑程序设计(inductive logic programming, ILP)是以一阶逻辑归纳理论为基础,并以一阶逻辑为表达语言的符号规则学习方法. ILP学得的模型是易于理解的一阶逻辑符号规则,而非难以解释的黑箱模型;在学习中可以相对容易地显式利用以一阶逻辑描述的领域知识;学得模型能对领域中个体间的关系进行建模,而非仅仅对个体的标记进行预测. 然而,由于潜在假设空间巨大,进行高效学习有相当的困难.综述了ILP领域的研究情况,从不同一阶逻辑归纳理论的角度对主流的ILP方法做出了梳理.还介绍了近年来ILP基于二阶诱导推理理论的扩展、基于概率的扩展和引入可微构件的扩展.最后,介绍了ILP在实际任务中的代表性应用,探讨了ILP方法目前所遇到的挑战,并对其未来发展进行了展望.     

一阶逻辑在关系数据库中的应用

一阶逻辑能唯一地作为关系数据库的统一语言，对关系数据库的可用性很多，本文主要讨论一些利用Prolog语言实现的应用。     

Open Bisimulation, Revisited

In the context of the π-calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show in how far it coincides with the original one.     

关于并发系统分支互模拟关系发散性保持的研究

带发散性说明的分支互模拟是van Glabbeek和Weijland提出的一个概念,并被用来定义等价关系.该等价关系应该是最弱的一个发散性保持的并且满足分支互模拟性质的等价关系.然而在概念提出时并没有提供这些重要性质的证明,并且我们认为在原定义的基础上这个证明是不显然的.本文通过co-induction的手段利用染色迹的概念定义了着色完全迹等价,并证明该等价关系是最弱的一个保持发散的并且满足分支互模拟性质的等价关系.然后我们证明了着色完全迹等价关系和≈_b^△是相同的,因而补充了van Glabbeek和Weijland的工作,即证明了≈_b^△是最弱的一个保持发散的并且是满足分支互模拟性质的等价关系.     

Bisimulation from Open Maps

An abstract definition of bisimulation is presented. It makes possible a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets), and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a strengthening of the history-preserving bisimulation of Rabinovitch and Traktenbrot and van Glabeek and Goltz. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has “refinement” operators. The general approach yields a logic, generalising Hennessy–Milner logic, which is characteristic for the generalised notion of bisimulation.     

Bisimulation and Hidden Algebra

A hidden algebra is a special case of coalgebra. A hidden congruence on a hidden algebra corresponds to a bisimulation equivalence on the corresponding coalgebra. The paper generalizes the notion of hidden congruence to that of hidden bisimulation between two different hidden algebras. We first define hidden bisimulation between two hidden algebras having the same signature. A hidden bisimulation is in fact a bisimulation between the corresponding coalgebras. We then define hidden simulation between two hidden algebras having different signatures related by a vertical signature morphism. We prefer to call this relation simulation because it is unidirectional, due to the signature morphism. For the last case, the relationship between simulation and refinement is discussed.     

Bisimulation is two-way simulation

We give here a simple proof of the fact that on transition systems bisimulation is the equivalence relation generated by simulation via functions. The proof entirely rests on simple rules of the calculus of relations.     

非对称χ≠-演算的互模拟格

非对称χ≠-演算是一种移动计算模型.通过研究该演算的互模拟格,能够增强理解非对称性和不等名算子对移动进程代数理论的影响.在给出非对称χ≠-演算的语法和转移语义系统的基础上,定义了该演算的L-互模拟关系.研究表明非对称χ≠-演算的63个L-互模拟关系重叠为12个不同的互模拟关系,而且这12个互模拟关系构成了一个关于集包含的互模拟格.最后证明了barbed互模拟和开互模拟分别与该互模拟格的顶元和底元互模拟关系相重合.     

Bisimulation for Labelled Markov Processes

In this paper we introduce a new class of labelled transition systems—labelled Markov processes— and define bisimulation for them. Labelled Markov processes are probabilistic labelled transition systems where the state space is not necessarily discrete. We assume that the state space is a certain type of common metric space called an analytic space. We show that our definition of probabilistic bisimulation generalizes the Larsen–Skou definition given for discrete systems. The formalism and mathematics is substantially different from the usual treatment of probabilistic process algebra. The main technical contribution of the paper is a logical characterization of probabilistic bisimulation. This study revealed some unexpected results, even for discrete probabilistic systems.

• Bisimulation can be characterized by a very weak modal logic. The most striking feature is that one has no negation or any kind of negative proposition.

• We do not need any finite branching assumption, yet there is no need of infinitary conjunction.

We also show how to construct the maximal autobisimulation on a system. In the finite state case, this is just a state minimization construction. The proofs that we give are of an entirely different character than the typical proofs of these results. They use quite subtle facts about analytic spaces and appear, at first sight, to be entirely nonconstructive. Yet one can give an algorithm for deciding bisimilarity of finite state systems which constructs a formula that witnesses the failure of bisimulation.     

Bisimulation for Higher-Order Process Calculi

Ahigher-order process calculusis a calculus for communicating systems which contains higher-order constructs like communication of terms. We analyse the notion ofbisimulationin these calculi. We argue that both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well ashigher-order bisimulation[E. Astesiano, A. Giovini, and G. Reggio,in“STACS '88,” Lecture Notes in Computer Science, Vol. 294, pp. 207–226, Springer-Verlag, Berlin/New York, 1988; G. Boudol,in“TAPSOFT '89,” Lecture Notes in Computer Science, Vol. 351, pp. 149–161, Springer-Verlag, Berlin/New York, 1989; B. Thomsen, Ph.D. thesis, Dept. of Computing, Imperial College, 1990] are in general unsatisfactory, because of their over-discrimination. We propose and study a new form of bisimulation for such calculi, calledcontext bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition, which is hard to handle in practice. To resolve this difficulty we introducetriggered bisimulationandnormal bisimulation, and we prove that they both coincide with context bisimulation. In the proof, we exploit thefactorisation theorem: When comparing the behaviour of two processes, it allows us to “isolate” subcomponents which might give differences, so that the analysis can be concentrated on them     

Notes on Generative Probabilistic Bisimulation

In this notes we consider the model of Generative Probabilistic Transition Systems, and Baier and Hermanns' notion of weak bisimulation defined over them. We prove that, if we consider any process algebra giving rise to a Probabilistic Transition System satisfying the condition of regularity and offering prefixing, interleaving, and guarded recursion, then the coarsest congruence that is contained in weak bisimulation is strong bisimulation.