Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus

We present a call-by-need λ-calculus λ_ND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ_≈, since the naïve bisimulation definition is useless. The main result is that bisimulation in λ_≈ is a congruence and coincides with the contextual equivalence. The proof is a non-trivial extension of Howe's method. This might be a step towards defining useful bisimulation relations and proving them to be congruences in calculi that extend the λ_ND-calculus.     

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

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

一种改进的安全环境演算及其行为等价关系研究

移动计算是在网络技术发展过程中涌现出来的一种新的分布计算范型．移动环境演算是一种广为使用的描述移动计算的形式化模型．安全环境演算为每个动作原语增加了一个相应的协动作原语,从而解决了强干扰问题．然而,SA的语法定义在直觉上并不能很好地描述out原语的协动作,同时其代数性质也存在一些缺陷．针对这些问题,一方面调整了SA的归约关系,将出入动作的语义统一在“进入时检查”这一约定之下,使其更符合直觉含义．在此基础上,通过采用Honda—Yoshida的技术,定义开接口互模拟等价关系,修正了SA代数性质上的缺陷,并通过一个防火墙的饲子说明了改进的安全环境演算及其行为等价关系的合理性．     

Backward Bisimulation in Markov Chain Model Checking

Equivalence relations can be used to reduce the state space of a system model, thereby permitting more efficient analysis. We study backward stochastic bisimulation in the context of model checking continuous-time Markov chains against continuous stochastic logic (CSL) properties. While there are simple CSL properties that are not preserved when reducing the state space of a continuous-time Markov chain using backward stochastic bisimulation, we show that the equivalence can nevertheless be used in the verification of a practically significant class of CSL properties. We consider an extension of these results to Markov reward models and continuous stochastic reward logic. Furthermore, we identify the logical properties for which the requirement on the equality of state-labeling sets (normally imposed on state equivalences in a model-checking context) can be omitted from the definition of the equivalence, resulting in a better state-space reduction     

Proving Congruence of Bisimulation in Functional Programming Languages

We give a method for proving congruence of bisimulation-like equivalences in functional programming languages. The method applies to languages that can be presented as a set of expressions together with an evaluation relation. We use this method to show that some generalizations of Abramsky's applicative bisimulation are congruences whenever evaluation can be specified by a certain natural form of structured operational semantics. One of the generalizations handles nondeterminism and diverging computations.     

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.     

Planning Proofs of Equations in CCS

Most efforts to automate formal verification of communicating systems have centred around finite-state systems (FSSs). However, FSSs are incapable of modelling many practical communicating systems, including a novel class of problems, which we call VIPS. VIPSs are value-passing, infinite-state, parameterised systems. Existing approaches using model checking over FSSs are insufficient for VIPSs. This is due to their inability both to reason with and about domain-specific theories, and to cope with systems having an unbounded or arbitrary state space.We use the Calculus of Communicating Systems (CCS) (Communication and Concurrency. London: Prentice Hall, 1989) to express and specify VIPSs. We take program verification to be proving the program and its intended specification equivalent. We use the laws of CCS to conduct the verification task. This approach allows us to study communicating systems and the data such systems communicate. Automating theorem proving in this context is an extremely difficult task.We provide automated methods for CCS analysis; they are applicable to both FSSs and VIPSs. Adding these methods to the CL ^A M proof planner (Lecture Notes in Artificial Intelligence, Vol. 449, Springer, 1990, pp. 647, 648), we have implemented an automated verification planner capable of dealing with problems that previously required human interaction. This paper describes these methods, gives an account as to why they work, and provides a short summary of experimental results.     

Weak and strong fairness in CCS

We examine the issue of weak and strong fairness in the framework of Milner's CCS. Our approach is operational. We address the problem of giving sets of finite rules for generating all and only the admissible execution sequences when fairness is assumed. We achieve our aims by defining two calculi, one for weak and the other for strong fairness. Both calculi are extensions of standard CCS. In neither case do we appeal to random assignment or to transformations. A distinguishing feature of the weak fair calculus, unlike standard approaches which appeal to random assignment, is that it does not involve predictive choice.     

A Completeness Proof for Bisimulation in the pi-calculus Using Isabelle

We use the interactive theorem prover Isabelle to prove that the algebraic axiomatization of bisimulation equivalence in the pi-calculus is sound and complete. This is the first proof of its kind to be wholly machine checked. Although the result has been known for some time the proof had parts which needed careful attention to detail to become completely formal. It is not that the result was ever in doubt; rather, our contribution lies in the methodology to prove completeness and get absolute certainty that the proof is correct, while at the same time following the intuitive lines of reasoning of the original proof. Completeness of axiomatizations is relevant for many variants of the calculus, so our method has applications beyond this single result. We build on our previous effort of implementing a framework for the pi-calculus in Isabelle using the nominal data type package, and strengthen our claim that this framework is well suited to represent the theory of the pi-calculus, especially in the smooth treatment of bound names.     

自动播控软件在硬盘播出系统中应用

随着计算机技术的不断发展,视音频服务器开始广泛应用于电视播出系统,电视播控进入了全硬盘时代。在这一高度自动化的领域中,计算机控制技术无可比拟的优越性得到了充分的体现,而相对于硬件来说,自动播控软件同样发挥着越来越重要的作用。     

Ambient Calculus and its Logic in the Calculus of Inductive Constructions

The Ambient Calculus has been recently proposed as a model of mobility of agents in a dynamically changing hierarchy of domains. In this paper, we describe the implementation of the theory and metatheory of Ambient Calculus and its modal logic in the Calculus of Inductive Constructions. We take full advantage of Higher-Order Abstract Syntax, using the Theory of Contexts a fundamental tool for developing formally the metatheory of the object system. Among others, we have successfully proved a set of fresh renamings properties, and formalized the connection between the Theory of Contexts and Gabbay-Pitts' “new” quantifier. As a feedback, we introduce a new definition of satisfaction for the Ambients logic and derive some of the properties originally assumed as axioms in the Theory of Contexts.     

Parametric channels via label expressions in CCS

CCS, the Calculus of Communicating Systems devised by Milner, has proved extremely successful for providing, via translation, a sound mathematical basis for a wide class of concurrent languages. Nevertheless, as it stands, it suffers from a limitation: it is impossible to determine at run time the channel on which to send or receive a communication. There are various possibilities for giving CCS such ability, but the price can be a drastic change in the language and the theory of CCS.Here we present a simple solution to this problem, which keeps language and theory almost unchanged, at least in fundamental aspects: the essential idea is to extend CCS by allowing (channel-) label expressions. We also show various applications of this extended version of CCS.     

Coinductive Counting: Bisimulation in Enumerative Combinatorics (Extended Abstract)

The recently developed coinductive calculus of streams finds here a further application in enumerative combinatorics. A general methodology is developed to solve a wide variety of basic counting problems in a uniform way: (1) the objects to be counted are enumerated by means of an infinite (weighted) automaton; (2) the automaton is minimized by means of the quantitative notion of stream bisimulation; (3) the minimized automaton is used to compute an expression (in terms of stream constants and operators) that represents the stream of all counts.     

Wormhole Broadcast in Hypercubes

We consider the problem of broadcasting a message in the n-cube, Q_n, equipped with wormhole switching. The communication model assumed is one-port, and the broadcasting scheme is path-based whereby, during broadcasting along a path by a node, all the nodes on that path will receive the message. The wormhole path length is m where –m's concurrently (cube-based broadcast). The second method is based on the concept of Gray codes (GCs), and at every given step, it forms the Hamiltonian path of appropriate size as the broadcast path (GC-based broadcast). It is shown that the steps required in GC-based broadcast is fewer than or equal to those needed by cube-based broadcast. Furthermore, comparison of time complexity of GC-based broadcast to the lower bound reveals that this algorithm is near-optimal, and in fact optimal in many cases. This work improves on the best algorithm developed for path-based broadcast in one-port hypercube both in complexity and in simplicity.     

动态代码检查及其在解释性语言中的应用

随着Internet以及分布式系统的不断发展和广泛应用,安全问题正在逐渐成为研究的热点。其中关于恶意代码所导致的软件安全问题也引起了人们的关注。该文重点分析了时序安全特性和竞争条件等代码分析热点问题,给出了时序安全特性的分类以及形式化描述,提出了将模式识别应用于解释性语言中的动态代码检查方法。将该方法应用于Perl语言解释器中,实现了对Perl语言脚本的动态检查.     

单元机组协调控制系统数学模型的研究及品质提升方法

单元机组协调控制系统中机炉对象的数学模型研究是近年来火力发电厂自动化技术研究中的热点,如何提高机组的负荷响匠速率,缩短负荷响应纯迟延时间,以及提高机组稳定性指标是电网和发电公司的共同目标。文章研究分析了近年来国内应用比较成功的工程技术方案和研究成果,对各方案的方法和结果做了类比,结合自身经验对应用成果中的非线性数学模型和线性数学模型环节的应用方法做了介绍。     

Broadcast in the rendezvous model

In many large, distributed or mobile networks, broadcast algorithms are used to update information stored at the nodes. In this paper, we propose a new model of communication based on rendezvous and analyze a multi-hop distributed algorithm to broadcast a message in a synchronous setting. In the rendezvous model, two neighbors u and v can communicate if and only if u calls v and v calls u simultaneously. Thus nodes u and v obtain a rendezvous at a meeting point. If m is the number of meeting points, the network can be modeled by a graph of n vertices and m edges. At each round, every vertex chooses a random neighbor and there is a rendezvous if an edge has been chosen by its two extremities. Rendezvous enable an exchange of information between the two entities. We get sharp lower and upper bounds on the time complexity in terms of number of rounds to broadcast: we show that, for any graph, the expected number of rounds is between ln n and O (n²). For these two bounds, we prove that there exist some graphs for which the expected number of rounds is either O (ln (n)) or Ω (n²). For specific topologies, additional bounds are given.     

Generating BDDs for symbolic model checking in CCS

Summary Finite transition systems can easily be represented by binary decision diagrams (BDDs) through the characteristic function of the transition relation. Burch et al. have shown how model checking of a powerful version of the -calculus can be performed on such BDDs. In this paper we show how a BDD can be generated from elementary finite transition systems given as BDDs by applying the CCS operations of parallel composition, restriction, and relabelling. The resulting BDDs only grow linearly in the number of parallel components. This way bisimilarity checking can be performed for processes out of the reach of conventional process algebra tools. Reinhard Enders graduated from the Technical University in Munich with a Diploma in mathematics and computer science in 1978. From 1977 to 1984 he was employed by Siemens, working in computer linguistics and expert systems. From 1984 to 1988 he worked at ECRC on Prolog extensions. In Autmn 1988 he joined Siemens and is developping the constraint extension of a new Prolog product. Thomas Filkorn received the computer science degree and the Ph.D. degree, both from the Technical University of Munich. Since 1992 he works at Siemens' Corporate Research and Development on symbolic algorithms and methods for the verification of finite state systems. Dirk Taubner received his Ph.D. in informatics at the Technical University of Munich in 1988. He investigated which sublanguages of process algebra could be represented finitely by automata and Petri nets. From 1989 through 91 he worked at Siemens' Corporate Research and Development where he led a project on computer-aided verification of parallel processes. This paper presents part of the work of that project. Currently he works on commercial software engineering for a software consulting company.