Equivalences for a biological process algebra

This paper investigates Bio-PEPA, the stochastic process algebra for biological modelling developed by Ciocchetta and Hillston. It focuses on Bio-PEPA with levels where molecular counts are grouped or concentrations are discretised into a finite number of levels. Basic properties of well-defined Bio-PEPA systems are established after which equivalences used for the stochastic process algebra PEPA are considered for Bio-PEPA, and are shown to be identical for well-defined Bio-PEPA systems. Two new semantic equivalences parameterised by functions, called g-bisimilarity and weak g-bisimilarity are introduced. Different functions lead to different equivalences for Bio-PEPA. Congruence is shown for both forms of g-bisimilarity under certain reasonable conditions on the function and the use of these equivalences are demonstrated with a biologically-motivated example where two similar species are treated as a single species, and modelling of alternative pathways in the MAPK kinase signalling cascade.     

Revisiting timing in process algebra

We shortly review the framework of process algebras with timing presented by Baeten and Middelburg [Handbook of Process Algebra, Elsevier, 2001, Chapter 10]. In order to cover processes that are capable of performing certain actions at all points in some time interval, we add integration to the process algebra with continuous relative timing from this framework. This extension happens to reveal some points that are peculiar to relative timing. We go into these points. The most flagrant point is that, unlike in case of absolute timing, discretization cannot be added to the extension without first adding a mechanism for parametric timing like initial abstraction.     

What is a free name in a process algebra?

There are two popular approaches to specifying the semantics of process algebras: labelled transition semantics and reaction semantics. While the notion of free name is rather unproblematic for labelled transition semantics this is not so for reaction semantics in the presence of a structural congruence for unfolding recursive declarations.We show that the standard definition of free name is not preserved under the structural congruence. We then develop a fixed point approach to the set of free names and show that it is invariant under the structural congruence.     

Duplication of constants in process algebra

The constant 0 (or δ, nil) has different roles in process algebra: on the one hand, it serves as the identity element of alternative composition, on the other hand, it stands for a blocked atomic action or for livelock. When extensions with timing are considered, these roles diverge. We argue that it is better to use two separate constants 0˙ and 0 for the different usages.With respect to the termination constant 1 (or , skip), the situation is comparable: on the one hand, it serves as the identity element of sequential composition, on the other hand, it serves as the identity element of parallel composition, and stands for a skipped atomic action. We have separate constants 1˙ and 1 for the different usages.We set up a theory of process algebra, starting out from these four constants in their respective roles. We do this first for the untimed theory, and work out the extension to discrete timing and relative timing in detail. We indicate how extensions involving dense timing or absolute timing are to be handled. All extensions are conservative.     

Real space process algebra

The real time process algebra of Baeten and Bergstra [Formal Aspects of Computing,3, 142–188 (1991)] is extended to real space by requiring the presence of spatial coordinates for each atomic action, in addition to the required temporal attribute. It is found that asynchronous communication cannot easily be avoided. Based on the state operators of Baeten and Bergstra [Information and Computation,78, 205–245 (1988)] and following Bergstra et al. [Proc. Seminar on Concurrency, LNCS 197, Springer, 1985, pp. 76–95], asychronous communication mechanisms are introduced as an additional feature of real space process algebra. The overall emphasis is on the introductory explanation of the features of real space process algebra, and characteristic examples are given for each of these.     

Discrete time process algebra

The axiom system ACP of [BeK84a] was extended with real time features in [BaB91]. Here we proceed to define a discrete time extension of ACP, along the lines of ATP [NiS94]. We present versions based on relative timing and on absolute timing. Both approaches are integrated using parametric timing. The time free ACP theory is embedded in the discrete time theory.     

Real time process algebra

We describe an axiom system ACP _p that incorporates real timed actions. Many examples are provided in order to explain the intuitive contents of the notation. ACP _p is a generalisation of ACP. This implies that some of the axioms have to be relaxed and that ACP can be recovered as a special case from it. The purpose of ACP _p is to serve as a specification language for real time systems. The axioms of ACP _p explain its operational meaning in an algebraic form.     

Priority and abstraction in process algebra

More than 15 years ago, Cleaveland and Hennessy proposed an extension of the process algebra CCS in which some actions may take priority over others. The theory was equipped with a behavioral congruence based on strong bisimulation.This article gives a full account of the challenges in, and the solutions employed for, defining a semantic theory of observation congruence for this process algebra. A full-abstraction result is presented whose proof relies on a novel approach based on successive approximations for identifying the largest congruence contained in an intuitive but naïve equivalence. Prioritized observation congruence is also characterized equationally for the class of finite processes, while its utility for system verification is demonstrated by an illustrative example.     

Timing and causality in process algebra

 There has been considerable controversy in concurrency theory between the ‘interleaving’ and ‘true concurrency’ schools. The former school advocates associating a transition system with a process which captures concurrent execution via the interleaving of occurrences; the latter adopts more complex semantic structures to avoid reducing concurrency to interleaving. In this paper we show that the two approaches are not irreconcilable. We define a timed process algebra where occurrences are associated with intervals of time, and give it a transition system semantics. This semantics has many of the advantages of the interleaving approach; the algebra admits an expansion theorem, and bisimulation semantics can be used as usual. Our transition systems, however, incorporate timing information, and this enables us to express concurrency: merely adding timing appropriately generalises transition systems to asynchronous transition systems, showing that time gives a link between true concurrency and interleaving. Moreover, we can provide a complete axiomatisation of bisimulation for our algebra; a result that is often problematic in a timed setting. Another advantage of incorporating timing information into the calculus is that it allows a particularly simple definition of action refinement; this we present. The paper concludes with a comparison of the equivalence we present with those in the literature, and an example system specification in our formalism. Received December 20, 1993/February 23, 1995     

A fair distributed mutual exclusion algorithm

This paper presents a fair decentralized mutual exclusion algorithm for distributed systems in which processes communicate by asynchronous message passing. The algorithm requires between N-1 and 2(N-1) messages per critical section access, where N is the number of processes in the system. The exact message complexity can be expressed as a deterministic function of concurrency in the computation. The algorithm does not introduce any other overheads over Lamport's and Ricart-Agrawala's algorithms, which require 3(N-1) and 2(N-1) messages, respectively, per critical section access and are the only other decentralized algorithms that allow mutual exclusion access in the order of the timestamps of requests     

Design of a biomolecular device that executes process algebra

Process algebras are widely used for defining the formal semantics of concurrent communicating processes. This paper considers stochastic π-calculus which is a particularly expressive kind of process algebra providing a specification of probabilities of process behavior such as stochastic delays, communication and branching, as well as rates of execution. In this paper, we implement stochastic π-calculus at the molecular scale, providing a design for a DNA-based biomolecular device that executes the stochastic π-calculus. Designing this device is challenging due to the requirement that a specific pair of processes must be able to communicate repeatedly; this appears to rule out the use of many of the usual classes of DNA computation (e.g., tiling self-assembly or hybridization chain reactions) that allow computational rule molecules to float freely in solution within a test tube. Our design of the molecular stochastic π-calculus system makes use of a modified form of Whiplash-PCR (WPCR) machines. In our machine which we call π-WPCR machine, we connect (via a tethering DNA nanostructure) a number of DNA strands, each of which corresponds to a π-WPCR machines. This collection of π-WPCR machines is used to execute distinct concurrent processes, each with its own distinct program. To implement process communication protocols, our modifications to the original design of WPCR machines include the incorporation of additional secondary structure in the single strand (stem-loop) as well as multiple-temperature thermal cycling. The enforced locality of the collection of π-WPCR machines insures that the same pair (or any subset of the entire collection) of processes be able to repeatedly communicate with each other. Additionally, our design of the devices include implementation of sequential execution of multiple process and limited process branching through use of restriction enzymes.     

一种新型的网络包公平调度算法的研究*

针对现有分组轮转法的局限,提出一种新的分组策略——虚拟权重队列分组策略。在这个新的分组策略的基础上,结合DRR和WF2Q,提出了虚拟权重队列分组轮转法。仿真实验表明,虚拟权重队列分组轮转调度算法比现有的分组轮转法拥有更好的延时性能和公平性能。     

多处理器系统的实时调度算法研究

调度算法是实时系统的关键技术,选取何种算法调度实时任务,这将直接影响着系统的实时响应能力。多处理器系统有局部调度和全局调度两类实时调度方法,以PFair公平调度为代表的全局调度是当前研究的热点。研究了典型局部调度EDF-FF算法和典型PFair公平调度PD^2算法,比较了多处理器系统采用PD^2算法相对于采用EDF-FF算法实现任务调度的优点,分析了由于任务频繁抢占和迁移,PD^2算法引起的时间消耗,估计并比较了PD2算法和EDF-FF算法的时间消耗,最后得出结论：在共享内存的多处理器系统中,公平调度算法是实时任务调度的比较理想的选择。     

基于支持向量机体温检测模型的活性判别算法

提出了一种基于支持向量机体温检测模型的活性判别算法.该算法通过大量的人体前额和腋下温度的样本来训练基于支持向量机的体温检测模型,然后在活性判别过程中,通过检测被识别人的体温来完成活性判别的过程.由于人脸照片的温度不可能与正常人的体温相同,所以照片就被成功的排除在了人脸识别系统的外面,从而提高了人脸自动识别系统的安全性,而且在活性判别过程中,被识别人不需要做表情或者是姿态的变化来配合识别,极大的方便了被识别者,增强了人脸识别系统的方便性.     

An algebra for process creation

In this paper, we study the issue of process creation from an algebraic perspective. The key to our approach, which is inspired by work of America and De Bakker, consists of giving a new interpretation to the operator symbol · (sequential composition) in the axiom system BPA of Bergstra and Klop. We present a number of other models for BPA and show how the new interpretation of · naturally generalises the usual interpretation in ACP. We give an operational semantics based on Plotkin style inductive rules for a simple language with process creation and communication, and give a complete finite axiomatisation of the associated bisimulation model. Note: Partial support received from the European Communities under ESPRIT contract 432, An Integrated Formal Approach to Industrial Software Development (METEOR), and RACE contract 1046, Specification and Programming Environment for Communication Software (SPECS).     

Encoding a process algebra using the Event B method

This paper presents the use of the B technique in its event based definition. We show that it is possible to encode, using Event B, the models (i.e., transition systems) associated to a process algebra with asynchronous semantics. The obtained Event B models consider that the Event B model associated to the left hand side of a BNF rule defining the algebra expressions is refined by a model corresponding to the right hand side of the same rule. The translation rules of each operator of a basic process algebra are given. Then, an example illustrating each translation rule is given. This approach is based on a proof technique and therefore it does not suffer from the state number explosion problem occurring in classical model checking. The interest of this work is the capability to validate user tasks or scenarios when using a given system and particularly a critical system. Finally, we discuss the application of this approach for validating user interfaces tasks in the human–computer interaction area.     

负载均衡的主导资源公平分配算法

随着使用云计算并行且可靠地处理计算问题成为一种趋势,各种云计算平台应运而生,在这些平台中,保证多种资源调度策略的公平性非常重要。主导资源公平分配算法DRF有效地实现了多种资源环境中的公平分配,但在资源分配过程中容易出现集群负载不均的情况。因此,提出在使用DRF算法分配资源过程中,通过集群中各节点的资源利用率情况对节点进行K-means聚类分析,根据聚类结果将资源分配给任务来提高集群负载均衡的能力。基于CloudSim 4.0实现了改进DRF算法的仿真实验,实验结果表明,负载均衡的DRF算法比原始的DRF算法以及基于层次分析法(AHP)改进的DRF算法更能有效地改善集群整体的负载均衡。