O-Minimal Hybrid Systems

An important approach to decidability questions for verification algorithms of hybrid systems has been the construction of a bisimulation. Bisimulations are finite state quotients whose reachability properties are equivalent to those of the original infinite state hybrid system. In this paper we introduce the notion of o-minimal hybrid systems, which are initialized hybrid systems whose relevant sets and flows are definable in an o-minimal theory. We prove that o-minimal hybrid systems always admit finite bisimulations. We then present specific examples of hybrid systems with complex continuous dynamics for which finite bisimulations exist. Date received: June 9, 1998. Date revised: June 28, 1999.     

Bisimilar linear systems

The notion of bisimulation in theoretical computer science is one of the main complexity reduction methods for the analysis and synthesis of labeled transition systems. Bisimulations are special quotients of the state space that preserve many important properties expressible in temporal logics, and, in particular, reachability. In this paper, the framework of bisimilar transition systems is applied to various transition systems that are generated by linear control systems. Given a discrete-time or continuous-time linear system, and a finite observation map, we characterize linear quotient maps that result in quotient transition systems that are bisimilar to the original system. Interestingly, the characterizations for discrete-time systems are more restrictive than for continuous-time systems, due to the existence of an atomic time step. We show that computing the coarsest bisimulation, which results in maximum complexity reduction, corresponds to computing the maximal controlled or reachability invariant subspace inside the kernel of the observations map. These results establish strong connections between complexity reduction concepts in control theory and computer science.     

Towards a theory of bisimulation for the higher-order process calculi

In this paper, a labelled transition semantics for higher-order process calculi is studied. The labelled transition semantics is relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. And the congruence properties of the bisimulation equivalence can be proved easily. To show the correspondence between the proposed semantics and the well-established ones, the bisimulation is characterized as a version of barbed equivalence and a version of context bisimulation.     

Probabilistic bisimulations for quantum processes

Modeling and reasoning about concurrent quantum systems is very important for both distributed quantum computing and quantum protocol verification. As a consequence, a general framework formally describing communication and concurrency in complex quantum systems is necessary. For this purpose, we propose a model named qCCS. It is a natural quantum extension of classical value-passing CCS which can deal with input and output of quantum states, and unitary transformations and measurements on quantum systems. The operational semantics of qCCS is given in terms of probabilistic labeled transition system. This semantics has many different features compared with the proposals in the available literature in order to describe the input and output of quantum systems which are possibly correlated with other components. Based on this operational semantics, the notions of strong probabilistic bisimulation and weak probabilistic bisimulation between quantum processes are introduced. Furthermore, some properties of these two probabilistic bisimulations, such as congruence under various combinators, are examined.     

Contextual Labelled Semantics for Higher-order Process Calculi

In this paper, we study a contextual labelled transition semantics for Higher-Order process calculi. The labelled transition semantics are relatively clean and simple, and corresponding bisimulation equivalence can be easily formulated based on it. Besides we develop a novel approach to reason about behaviours of a higher-order substituted process P{Q/X}, based on which we can directly prove a very important result – factorisation theorem. To show the correspondence between our semantics and the well-established ones, we characterize our bisimulation in a version of barbed equivalence.     

传值系统的互模拟与谓词等式系

本文引入描述传值并系统的新模型“带赋值符号迁移图（ＳＴＧＡ）”推广了Ｈｅｎｎｅｓｓｙ和Ｌｉｎ提出的“符号迁移图”的概念，允许迁移上带有赋值，从而能将更大的一类传值系统表示为有穷状态图，ＳＴＧＡ的中车优点是在并行运算不封闭，文中给给ＳＴＧＡ的操作语义，在此基础上定义了ＳＴＧＡ的互模拟等价关系，为了刻划ＳＴＧＡ的互模拟，以谓词等式系的形式在一阶逻辑的正子集中扩充了最大和最小不动点，并设计了一个算法将Ｓ     

Models for name-passing processes: interleaving and causal

We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.     

Exploring probabilistic bisimulations, part I

We take a fresh look at strong probabilistic bisimulations for processes which exhibit both non-deterministic and probabilistic behaviour. We suggest that it is natural to interpret such processes as distributions over states in a probabilistic labelled transition system, a pLTS; this enables us to adapt the standard notion of contextual equivalence to this setting. We then prove that a novel form of bisimulation equivalence between distributions are both sound and complete with respect to this contextual equivalence. We also show that a very simple extension to HML, Hennessy–Milner Logic, provides finite explanations for inequivalences between distributions. Finally we show that our bisimulations between distributions in a pLTS are simply an alternative characterisation of a standard notion of probabilistic bisimulation equivalence, defined between states in a pLTS.     

On the observational theory of the CPS-calculus

We apply powerful proof-techniques of concurrency theory to study the observational theory of Thielecke’s CPS-calculus, a distillation of the target language of Continuation-Passing Style transforms. We define a labelled transition system from which we derive a (weak) labelled bisimilarity that completely characterises Morris’ context-equivalence. We prove a context lemma showing that Morris’ context-equivalence coincides with a simpler context-equivalence closed under a smaller class of contexts. Then we profit of the determinism of the CPS-calculus to give a simpler labelled characterisation of Morris’ equivalence, in the style of Abramsky’s applicative bisimilarity. We enhance our bisimulation proof-methods with up to bisimilarity and up to context proof techniques. We use our bisimulation proof techniques to investigate a few algebraic properties on diverging terms that cannot be proved using the original axiomatic semantics of the CPS-calculus.     

基于符号迁移图的互模拟验证算法

符号迁移图是传值进程的一种直观而简洁的语义表示模型，该模型由Hennessy和Lin首先提出，随后又被Lin推广至带赋值的符号迁移图，本文不但定义了符号迁移图各种版本（基／符号）的强操作语义和强互模拟，提出了相互的强互模拟算法，而且通过引入符号观察图和符号同余图，给出了其弱互模拟等价和观察同余的验证算法，给出并证明了了τ－循环和τ－边消去定理，在应用任何弱互模拟观察同余验证算法之前，均可利用这些定理对所给符号迁移图进行化简。     

An Observational Theory for Mobile Ad Hoc Networks (full version)

We propose a process calculus to study the behavioural theory of Mobile Ad Hoc Networks. The operational semantics of our calculus is given both in terms of a Reduction Semantics and in terms of a Labelled Transition Semantics. We prove that the two semantics coincide. The labelled transition system is then used to derive the notions of (weak) simulation and bisimulation for ad hoc networks. The labelled bisimilarity completely characterises reduction barbed congruence, a standard branching-time and contextually-defined program equivalence. We then use our (bi)simulation proof method to formally prove a number of non-trivial properties of ad hoc networks.     

A Syntactical Approach to Weak (Bi-)Simulation for Coalgebras

In [19] Rutten introduced the notion of weak bisimulations and weak bisimilarity for coalgebras of the functor F(X) = X + O. In the present paper I will introduce a notion of weak bisimulation for coalgebras based on the syntax of their functors for a large class of functors. I will show that my definition does not only coincide with the definition from [19], but with the definition for labelled transition systems as well. The approach includes a definition of weak bisimulation for Kripke structures, which might be of interest in its own right.     

Language-based Performance Prediction for Distributed and Mobile Systems

We present a framework for performance prediction of distributed and mobile systems. We rely on process calculi and their structural operational semantics. The dynamic behaviour is described through transition systems whose transitions are labelled by encodings of their proofs that we then map into stochastic processes. We enhance related works by allowing general continuous distributions resorting to a notion of enabling between transitions. We also discuss how the number of resources available affects the overall model. Finally, we introduce a notion of bisimulation that takes stochastic information into account and prove it to be a congruence. When only exponential distributions are of interest our equivalence induces a lumpable partition on the underlying Markov process.     

Deadlock Behaviour in Split and ST Bisimulation Semantics

We investigate split and ST bisimulation semantics, in particular the deadlock behaviour of processes in these semantics. We define and axiomatise a variant of ACP, where atomic actions and durational actions coexist, and define split and ST bisimulation semantics on this theory. We exhibit a closed term that has a deadlock in split semantics, but not in ST bisimulation semantics, and vice versa: a closed term that has a deadlock in ST bisimulation semantics but not in split semantics. As an application, we investigate different versions of durational communication.     

Verification of infinite-state dynamic systems using approximatequotient transition systems

This paper deals with computational methods for verifying properties of labeled infinite-state transition systems using quotient transition system (QTS). A QTS is a conservative approximation to the infinite-state transition system based on a finite partition of the infinite state space. For universal specifications, positive verification for a QTS implies the specification is true for the infinite-state transition system. We introduce the approximate QTS or AQTS. The paper presents a sufficient condition for an AQTS to be a bisimulation of the infinite state transition system. An AQTS bisimulation is essentially equivalent to the infinite-state system for the purposes of verification. It is well known, however, that finite-state bisimulations do not exist for most hybrid systems of practical interest. Therefore, the use of the AQTS for verification of universal specifications is proposed and illustrated with an example. This approach has been implemented in a tool for computer-aided verification of a general class of hybrid systems     

Computing maximal weak and other bisimulations

We present and compare several algorithms for computing the maximal strong bisimulation, the maximal divergence-respecting delay bisimulation, and the maximal divergence-respecting weak bisimulation of a generalised labelled transition system. These bisimulation relations preserve CSP semantics, as well as the operational semantics of programs in other languages with operational semantics described by such GLTSs and relying only on observational equivalence. They can therefore be used to combat the space explosion problem faced in explicit model checking for such languages. We concentrate on algorithms which work efficiently when implemented rather than on ones which have low asymptotic growth.     

Computing strong and weak bisimulations for psi-calculi

We present a symbolic transition system and strong and weak bisimulation equivalences for psi-calculi, and show that they are fully abstract with respect to bisimulation congruences in the non-symbolic semantics. A procedure which computes the most general constraint under which two agents are bisimilar is developed and proved correct.A psi-calculus is an extension of the pi-calculus with nominal data types for data structures and for logical assertions representing facts about data. These can be transmitted between processes and their names can be statically scoped using the standard pi-calculus mechanism to allow for scope migrations. Psi-calculi can be more general than other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, or the concurrent constraint pi-calculus.Symbolic semantics are necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means the symbolic semantics makes exactly the same distinctions as the original.     

生成诊断公式的有限状态进程等价验证

分析有限状态进程互模拟等价判定技术,探讨了诊断公式的生成问题.给出了将有限状态进程转化为带标号的迁移系统,修改了Paige和Trajan求解最粗划分的算法,使其适用于带标号的迁移系统.给出生成Hennessy-Milner逻辑描述的诊断公式的算法,当两个进程不能互模拟时,产生两个诊断公式.算法的时间复杂度为O(m log n),空间复杂度为O(m+n).     

Complete Proof Systems for Amortised Probabilistic Bisimulations

The notion of amortisation has been integrated in quantitative bisimulations to make long-term behavioral comparisons between nondeterministic systems. In this paper, we present sound and complete proof systems for amortised strong probabilistic bisimulation and its observational congruence on a process algebra with probability and nondeterminism, and prove their soundness and completeness. Our results make it possible to reason about long-term (observable) probabilistic behaviors by syntactic manipulations.