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 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.     

Characterizing contextual equivalence in calculi with passivation

We study the problem of characterizing contextual equivalence in higher-order languages with passivation. To overcome the difficulties arising in the proof of congruence of candidate bisimilarities, we introduce a new form of labeled transition semantics together with its associated notion of bisimulation, which we call complementary semantics. Complementary semantics allows to apply the well-known Howe?s method for proving the congruence of bisimilarities in a higher-order setting, even in the presence of an early form of bisimulation. We use complementary semantics to provide a coinductive characterization of contextual equivalence in the HOπP calculus, an extension of the higher-order π-calculus with passivation, obtaining the first result of this kind. We then study the problem of defining a more effective variant of bisimilarity that still characterizes contextual equivalence, along the lines of Sangiorgi?s notion of normal bisimilarity. We provide partial results on this difficult problem: we show that a large class of test processes cannot be used to derive a normal bisimilarity in HOπP, but we show that a form of normal bisimilarity can be defined for HOπP without restriction.     

A modal characterization of alternating approximate bisimilarity

Recently, alternating transition systems are adopted to describe control systems with disturbances and their finite abstract systems. In order to capture the equivalence relation between these systems, a notion of alternating approximate bisimilarity is introduced. This paper aims to establish a modal characterization for alternating approximate bisimilarity. Based on this result, we provide a link between specifications satisfied by the samples of control systems with disturbances and their finite abstractions. Moreover, a simple example is given to illustrate the application of such link in the design of controller of control systems.     

Mobility control via passports

Dπ is a simple distributed extension of the π-calculus in which agents are explicitly located, and may use an explicit migration construct to move between locations.In this paper, we introduce passports to control those migrations; in order to gain access to a location agents are now expected to show some credentials, granted by the destination location. Passports are tied to specific locations, from which migration is permitted. We describe a type system for these passports, which includes a novel use of dependent types, and prove that well-typing enforces the desired behaviour in migrating processes.Passports allow locations to control incoming processes. This induces major modifications to the observations which can be made of agent-based systems. Using the type system we describe these observations, and use them to build a loyal notion of observational equivalence for this setting. Finally we provide a complete proof technique in the form of a bisimilarity for establishing equivalences between systems.     

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.     

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.     

Deciding orthogonal bisimulation

Bergstra, Ponse and van der Zwaag introduced in 2003 the notion of orthogonal bisimulation equivalence on labeled transition systems. This equivalence is a refinement of branching bisimulation, in which consecutive tau’s (silent steps) can be compressed into one (but not zero) tau’s. The main advantage of orthogonal bisimulation is that it combines well with priorities. Here we solve the problem of deciding orthogonal bisimulation equivalence in finite (regular) labeled transition systems. Unlike as in branching bisimulation, in orthogonal bisimulation, cycles of silent steps cannot be eliminated. Hence, the algorithm of Groote and Vaandrager (1990) cannot be adapted easily. However, we show that it is still possible to decide orthogonal bisimulation with the same complexity as that of Groote and Vaandrager’s algorithm. Thus if n is the number of states, and m the number of transitions then it takes O(n(m + n)) time to decide orthogonal bisimilarity on finite labeled transition systems, using O(m + n) space. J. Parrow     

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

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

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.     

Linear and Branching System Metrics

We extend the classical system relations of trace inclusion, trace equivalence, simulation, and bisimulation to a quantitative setting in which propositions are interpreted not as boolean values, but as elements of arbitrary metric spaces. Trace inclusion and equivalence give rise to asymmetrical and symmetrical linear distances, while simulation and bisimulation give rise to asymmetrical and symmetrical branching distances. We study the relationships among these distances and we provide a full logical characterization of the distances in terms of quantitative versions of LTL and mu-calculus. We show that, while trace inclusion (respectively, equivalence) coincides with simulation (respectively, bisimulation) for deterministic boolean transition systems, linear and branching distances do not coincide for deterministic metric transition systems. Finally, we provide algorithms for computing the distances over finite systems, together with a matching lower complexity bound.     

A timed calculus for wireless systems

We propose a timed broadcasting process calculus for wireless systems where time-consuming communications are exposed to collisions. The operational semantics of our calculus is given in terms of a labelled transition system. The calculus enjoys a number of desirable time properties such as (i) time determinism: the passage of time is deterministic; (ii) patience: devices will wait indefinitely until they can communicate; (iii) maximal progress: data transmissions cannot be delayed, they must occur as soon as a possibility for communication arises. We use our calculus to model and study MAC-layer protocols with a special emphasis on collisions and security. The main behavioural equality of our calculus is a timed variant of barbed congruence, a standard branching-time and contextually-defined program equivalence. As an efficient proof method for timed barbed congruence we define a labelled bisimilarity. We then apply our bisimulation proof-technique to prove a number of algebraic laws.     

π-calculus with noisy channels

It is assumed in the π-calculus that communication channels are always noiseless. But it is usually not the case in the mobile systems that developers are faced with in the real life. In this paper, we introduce an extension of π, called π_N, in which noisy channels may be present. A probabilistic transitional semantics of π_N is given. The notions of approximate (strong) bisimilarity and equivalence between agents in π_N are proposed, and various algebraic laws for them are established. In particular, we introduce the notion of stratified bisimulation which is suited to describe behavior equivalence between infinite probabilistic processes. Some useful techniques for reasoning about approximate bisimilarity and equivalence are developed. We also introduce a notion of reliability in order to compare different behaviors of an agent in π and π_N. It is shown that reliability is preserved by the basic combinators in π. A link between reliability and bisimulation is given. This provides us with a uniform framework in which we can reason about both correctness properties and reliability of mobile systems. Also, a potential way of combing value-passing process algebras and Shannon’s information theory is pointed out.     

Branching Bisimulation Congruence for Probabilistic Systems

The notion of branching bisimulation for the alternating model of probabilistic systems is not a congruence with respect to parallel composition. In this paper we first define another branching bisimulation in the more general model allowing consecutive probabilistic transitions, and we prove that it is compatible with parallel composition. We then show that our bisimulation is actually the coarsest congruence relation included in the existing branching bisimulation when restricted to the alternating model.     

From SOS Specifications to Structured Coalgebras: How to Make Bisimulation a Congruence

In this paper we address the issue of providing a structured coalgebra presentation of transition systems with algebraic structure on states determined by an equational specification Γ. More precisely, we aim at representing such systems as coalgebras for an endofunctor on the category of Γ-algebras. The systems we consider are specified by using a quite general format of SOS rules, the algebraic format, which in general does not guarantee that bisimilarity is a congruence.We first show that the structured coalgebra representation works only for systems where transitions out of complex states can be derived from transitions out of corresponding component states. This decomposition property of transitions indeed ensures that bisimilarity is a congruence. For a system not satisfying this requirement, next we propose a closure construction which adds context transitions, i.e., transitions that spontaneously embed a state into a bigger context or vice-versa. The notion of bisimulation for the enriched system coincides with the notion of dynamic bisimilarity for the original one, that is, with the coarsest bisimulation which is a congruence. This is sufficient to ensure that the structured coalgebra representation works for the systems obtained as result of the closure construction.     

Bisimilarity Control of Partially Observed Deterministic Systems

Control for safety and nonblockingness using a deterministic supervisor requires the specification language be controllable and observable (under the setting that marking is also decided by a supervisor). We argue that there exist cases where the above properties do not hold, yet a safe and nonblocking control can be synthesized by allowing the supervisor to be nondeterministic. Use of a nondeterministic supervisor yields a controlled system that is nondeterministic for which a language equivalence only preserve the safety but not the nonblocking property, and so instead we require the stronger equivalence of bisimilarity (which preserves "sequential" behavior such as safety as well as "branching" behavior such as nonblockingness). This motivates us to consider control of deterministic systems for achieving bisimulation equivalence to possibly nondeterministic specifications. We introduce the notions of state-achievability (SA) and state-achievability-bisimilar (SAB) as part of the existence condition, and develop effective algorithms for verify the existence conditions as well as for synthesizing a supervisor when the existence condition holds. We show that the complexity of verifying the existence of a controller is polynomial, whereas that of computing a controller (when one exists) is singly exponential. The proposed approach can be applied to enforce any property that depends on branching and sequential behavior.     

Reactive systems, (semi-)saturated semantics and coalgebras on presheaves

The semantics of process calculi has traditionally been specified by labelled transition systems (ltss), but, with the development of name calculi, it turned out that reaction rules (i.e., unlabelled transition rules) are often more natural. This leads to the question of how behavioral equivalences (bisimilarity, trace equivalence, etc.) defined for lts can be transferred to unlabelled transition systems. Recently, in order to answer this question, several proposals have been made with the aim of automatically deriving an lts from reaction rules in such a way that the resulting equivalences are congruences. Furthermore, these equivalences should agree with the standard semantics, whenever one exists.In this paper, we propose saturated semantics, based on a weaker notion of observation and orthogonal to all the previous proposals, and we demonstrate the appropriateness of our semantics by means of two examples: logic programming and open Petri nets. We also show that saturated semantics can be efficiently characterized through the so called semi-saturated games. Finally, we provide coalgebraic models relying on presheaves.     

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 Small Model Theorem for Bisimilarity Control Under Partial Observation

This paper extends our prior result on decidability of bisimulation equivalence control from the setting of complete observations to that of partial observations. Besides being control compatible, the supervisor must now also be observation compatible. We show that the "small model theorem" remains valid by showing that a control and observation compatible supervisor exists if and only if it exists over a certain finite state space, namely the power set of the Cartesian product of the system and the specification state spaces. Note to Practitioners-Non-determinism in discrete-event systems arises due to abstraction and/or unmodeled dynamics. This paper addresses the issue of control of non-deterministic systems subject to non-deterministic specifications, under a partial observation of events. Non-deterministic plant and specification are useful when designing a system at a higher level of abstraction so that lower level details of the system and its specification are omitted to obtain higher level models that are non-deterministic. The control goal is to ensure that the controlled system has an equivalent behavior as the specification system, where the notion of equivalence used is that of bisimilarity. Bisimilarity requires the existence of an equivalence relation between the states of the two systems so that transitions on common events beginning from a pair of equivalent states end up in a pair of equivalent successor states. Supervisors are also allowed to be nondeterministic, where the nondeterminism in control is implemented by selecting control actions nondeterministically from among a set of precomputed choices. The main contribution of this paper is to show that a supervisor exists if and only if one exists where the size of its state-space upper bounded and so it suffices to search over this state space. We illustrate our results through a manufacturing example