Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach, while still offering compositional verification techniques.     

On the expressiveness and decidability of higher-order process calculi

In higher-order process calculi, the values exchanged in communications may contain processes. A core calculus of higher-order concurrency is studied; it has only the operators necessary to express higher-order communications: input prefix, process output, and parallel composition. By exhibiting a deterministic encoding of Minsky machines, the calculus is shown to be Turing complete. Therefore its termination problem is undecidable. Strong bisimilarity, however, is shown to be decidable. Furthermore, the main forms of strong bisimilarity for higher-order processes (higher-order bisimilarity, context bisimilarity, normal bisimilarity, barbed congruence) coincide. They also coincide with their asynchronous versions. A sound and complete axiomatization of bisimilarity is given. Finally, bisimilarity is shown to become undecidable if at least four static (i.e., top-level) restrictions are added to the calculus.     

Bisimilarity in Term Graph Rewriting

We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for different kinds of term graph rewriting; besides plain applications of rewrite rules, extensions with the operations of collapsing and copying, and both operations together are considered. Collapsing and copying together constitute bisimilarity of term graphs. We establish sufficient conditions for—and counterexamples to—confluence, confluence modulo bisimilarity, and the Church–Rosser property modulo bisimilarity. Moreover, we address rewriting modulo bisimilarity, that is, rewriting of bisimilarity classes of term graphs.     

(η,α)-互模拟的分层及判定算法

分层刻画是传统的互模拟概念研究中的一个重要内容,它为一些互模拟判定算法提供了理论基石。(η,α)-互模拟是一种带折扣的近似互模拟概念,其定义蕴涵着一种折扣思想:在比较系统差异时,越晚出现的差异越不重要。为(η,α)-互模拟建立分层刻画,将清晰地揭示这种折扣思想。此外,由于(η,α)-互模拟一般不是等价关系,所以传统的互模拟判定算法中常用的最粗划分方法不适用于(η,α)-互模拟的判定,基于(η,α)-互模拟的分层刻画给出一种该互模拟的判定算法。还提供一个简单的例子用于说明(η,α)-互模拟及其判定算法在描述实现与规范之间关系时的应用。     

Resource bisimilarity and graded bisimilarity coincide

Resource bisimilarity has been proposed in the literature on concurrency theory as a notion of bisimilarity over labeled transition systems that takes into account the number of choices that a system has. Independently, g-bisimilarity has been defined over Kripke models as a suitable notion of bisimilarity for graded modal logic. This note shows that these two notions of bisimilarity coincide over image-finite Kripke frames.     

On the axiomatizability of priority II

This paper contributes to the study of the equational theory of the priority operator of Baeten, Bergstra and Klop in the setting of the process algebra BCCSP. It is shown that, in the presence of at least two actions, the collection of process equations over BCCSP with the priority operator that are valid modulo bisimilarity, irrespective of the chosen priority order over actions, is not finitely based. This holds true even if one restricts oneself to the collection of valid process equations that do not contain occurrences of process variables.     

Resource bisimilarity and graded bisimilarity coincide

Resource bisimilarity has been proposed in the literature on concurrency theory as a notion of bisimilarity over labeled transition systems that takes into account the number of choices that a system has. Independently, g-bisimilarity has been defined over Kripke models as a suitable notion of bisimilarity for graded modal logic. This note shows that these two notions of bisimilarity coincide over image-finite Kripke frames.     

Equivalences for Silent Transitions in Probabilistic Systems: (Extended Abstract)

We address abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Together they give a better understanding of branching bisimilarity. A crucial observation, and, in fact a major motivation for this work is that the notions of branching bisimilarity in the alternating and in the non-alternating model differ, and that the latter one discriminates between systems that are intuitively branching bisimilar.     

Branching bisimulation for probabilistic systems: Characteristics and decidability

We address the concept of abstraction in the setting of probabilistic reactive systems, and study its formal underpinnings for the strictly alternating model of Hansson. In particular, we define the notion of branching bisimilarity and study its properties by studying two other equivalence relations, viz. coloured trace equivalence and branching bisimilarity using maximal probabilities. We show that both alternatives coincide with branching bisimilarity. The alternative characterisations have their own merits and focus on different aspects of branching bisimilarity. Coloured trace equivalence can be understood without knowledge of probability theory and is independent of the notion of a scheduler. Branching bisimilarity, rephrased in terms of maximal probabilities gives rise to an algorithm of polynomial complexity for deciding the equivalence. Together they give a better understanding of branching bisimilarity. Furthermore, we show that the notions of branching bisimilarity in the alternating model of Hansson and in the non-alternating model of Segala differ: branching bisimilarity in the latter setting turns out to discriminate between systems that are intuitively branching bisimilar.     

Decidability of Branching Bisimulation on Normed Commutative Context-Free Processes

We investigate normed commutative context-free processes (Basic Parallel Processes). We show that branching bisimilarity admits the bounded response property: in the Bisimulation Game, Duplicator always has a response leading to a process of size linearly bounded with respect to the Spoiler’s process. The linear bound is effective, which leads to decidability of branching bisimilarity. For weak bisimilarity, we are able merely to show existence of some linear bound, which is not sufficient for decidability. We conjecture however that the same effective bound holds for weak bisimilarity as well. We suppose that further elaboration of novel techniques developed in this paper may be sufficient to demonstrate decidability.     

Undecidability of domino games and hhp-bisimilarity

History preserving bisimilarity (hp-bisimilarity) and hereditary history preserving bisimilarity (hhp-bisimilarity) are behavioural equivalences taking into account causal relationships between events of concurrent systems. Their prominent feature is that they are preserved under action refinement, an operation important for the top-down design of concurrent systems. It is shown that, in contrast to hp-bisimilarity, checking hhp-bisimilarity for finite labelled asynchronous transition systems is undecidable, by a reduction from the halting problem of 2-counter machines. To make the proof more transparent a novel intermediate problem of checking domino bisimilarity for origin constrained tiling systems is introduced and shown undecidable. It is also shown that the unlabelled domino bisimilarity problem is undecidable, which implies undecidability of hhp-bisimilarity for unlabelled finite asynchronous systems. Moreover, it is argued that the undecidability of hhp-bisimilarity holds for finite elementary net systems and 1-safe Petri nets.     

A ground-complete axiomatization of stateless bisimilarity over Linda

This paper offers a finite, ground-complete axiomatization of stateless bisimilarity over the tuple-space-based coordination language Linda. As stepping stones towards that result, axiomatizations of stateless bisimilarity over the sequential fragment of Linda without the nask primitive, and over the full sequential sub-language are given. It is also shown that stateless bisimilarity coincides with standard bisimilarity over the sequential fragment of Linda without the nask primitive.     

Decidability of performance equivalence for basic parallel processes

We study an extension of the class of Basic Parallel Processes (BPP), in which actions are durational and urgent and parallel components have independent local clocks. The main result is decidability of strong bisimilarity, known also as performance equivalence, in this class. This extends the earlier decidability result for plain BPP by Christensen et al. Our decision procedure is based on decidability of the validity problem for Presburger arithmetic. We prove also polynomial complexity in positive-duration fragment, thus properly extending a previous result by Bérard et al. Both ill-timed and well-timed semantics are treated.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

Branching bisimulation congruence for probabilistic systems

A notion of branching bisimilarity for the alternating model of probabilistic systems, compatible with parallel composition, is defined. For a congruence result, an internal transition immediately followed by a non-trivial probability distribution is not considered inert. A weaker definition of branching bisimilarity for the same model has been given earlier. Here we show that our branching bisimulation is the coarsest congruence for parallel composition that is included in the weaker version. To support the use of the present equivalence as a reduction technique, we also show that probabilistic CTL formulae are preserved by our equivalence, and we provide a polynomial-time algorithm deciding branching bisimilarity.     

The Subgraph Similarity Problem

Similarity is a well known weakening of bisimilarity where one system is required to simulate the other and vice versa. It has been shown that the subgraph bisimilarity problem, a variation of the subgraph isomorphism problem where isomorphism is weakened to bisimilarity, is NP-complete. We show that the subgraph similarity problem and some related variations thereof still remain NP-complete.     

Causality versus true-concurrency

Category theory has been successfully employed to structure the confusing set-up of models and equivalences for concurrency: Winskel and Nielsen have related the standard models via adjunctions and (co)reflections while Joyal et al. have defined an abstract notion of equivalence, known as open map bisimilarity. One model has not been integrated into this framework: the causal trees of Darondeau and Degano. Here we fill this gap. In particular, we show that there is an adjunction from causal trees to event structures, which we bring to light via a mediating model, that of event trees. Further, we achieve an open map characterization of history preserving bisimilarity: the latter is captured by the natural instantiation of the abstract bisimilarity for causal trees.     

非确定型离散事件系统双模拟控制的实现

近年来,双模拟等价关系与离散事件系统监控理论相结合的研究引起了国内外许多学者的广泛关注.本文针对作者在前期工作中提出的非确定型离散事件系统的双模拟控制机制,进一步探讨其实现问题.利用投影映射对系统规范说明语言进行等价类划分,构造了一棵计算树,得到了一个判断规范说明是否具有基于模拟关系可观性的多项式算法,证明了双模拟控制机制是多项式时间算法可实现的.同时,通过对控制器配备具有存储和判断功能的模拟关系识别器,阐述了这种双模拟控制机制是物理可实现的.     

A hierarchy of probabilistic system types

We arrange various types of probabilistic transition systems studied in the literature in an expressiveness hierarchy. The expressiveness criterion is the existence of an embedding of systems of the one class into those of the other. An embedding here is a system transformation which preserves and reflects bisimilarity. To facilitate the task, we define the classes of systems and the corresponding notion of bisimilarity coalgebraically and use the new technical result that an embedding arises from a natural transformation with injective components between the two coalgebra functors under consideration. Moreover, we argue that coalgebraic bisimilarity, on which we base our results, coincides with the concrete notions proposed in the literature for the different system classes, exemplified by a detailed proof for the case of general Segala-type systems.     

Causality Versus True-Concurrency

Category theory has been successfully employed to structure the confusing setup of models and equivalences for concurrency: Winskel and Nielsen have related the standard models via adjunctions and (co)reflections while Joyal et al. have defined an abstract notion of equivalence, known as open map bisimilarity. One model has not been integrated into this framework: the causal trees of Darondeau and Degano. Here we fill this gap. In particular, we show that there is an adjunction from causal trees to event structures, which we bring to light via a mediating model, that of event trees. Further, we achieve an open map characterization of history preserving bisimilarity: the latter is captured by the natural instantiation of the abstract bisimilarity for causal trees.