A process algebra to formalize the Lyee methodology

Over the last years, various methodologies and techniques have been elaborated and proposed to improve one or many aspects related to the software development life cycle. However, despite the great effort in this research field, the production of clearly understood and modifiable systems still an ambitious goal and far from reached. This is due, on one hand, to the complexity and the subtlety of software themselves and, on the other hand, to the limitations of the current methodologies. Recently, a new and very promising methodology, called Lyee, has been proposed. Intended to deal efficiently with a wide range of software problems related to different field, Lyee allows the development of software by simply defining their requirements.

Nevertheless, since both the semantics of Lyee generated software together with the process of automatic generation of software from requirements are described using informal language, difficulties and confusions may arise when trying to understand and study this methodology.

The main purpose of this paper is to formalize, using a process algebra, the process of automatic generation of softwares together with the semantics of Lyee generated softwares. Actually, process algebra naturally supports many concepts of the Lyee methodology and consequently formalize them simply and elegantly. It offers to the Lyee methodology an abstract machine more suitable than the Von-Newman one. In fact, this new abstract machine consider a program as chemical solution when molecules (different vectors of the lyee methodology) interact together to reach a collective goal.     

The logic of message-passing

Message-passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message-passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the term calculus borrows heavily from the (synchronous) π-calculus. The cut-elimination procedure for the system provides an operational semantics.     

Bisimulations for a calculus of broadcasting systems

We develop a theory of bisimulation equivalence for the broadcast calculus CBS. Both the strong and weak versions of bisimulation congruence we study are justified in terms of a characterisation as the largest CBS congruences contained in an appropriate version of barbed bisimulation. We then present sound and complete proof systems for both the strong and weak congruences over finite terms. The first system we give contains an infinitary proof rule to accommodate input prefixes. We improve on this by presenting a unitary proof system where judgements are relative to properties of the data domain.     

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.     

A communicating sequential process language and implementation

The design of a communicating sequential process language is presented, featuring a parallel command, communication by message passing and the use of the guarded command as a means of introducing and controlling non-determinism. The language described here incorporates a number of new proposals regarding communications between sequential processes. The principal proposal is that messages are to be selected for reception by a receiving process solely on the basis of their type and arrival order within type; in particular, the identity of the sending process does not influence message reception. This results in a greater degree of parallelism and non-determinism, which is useful to both the programmer and the language implementor. Also a hierarchichal composition regime is proposed, which gives communications significance to the organization of subprocess hierarchies; this promotes an independence of specification of program components through information hiding properties. The language implementation is described, and several aspects are of particular interest: the design of a process scheduler in a non-deterministic situation leads to some interesting optimizations, as does the design of a message handler in the case where the communicating processes can access the same memory. Finally, example programs are given to illustrate some of the novel features of the language.     

Estimating the maximum information leakage

Preventing improper information leaks is a greatest challenge of the modern society. In this paper, we present a technique for measuring the ability of several families of adversaries to set up a covert channel. Our approach relies on a noninterference based formulation of security which can be naturally expressed by semantic models of the program execution. In our analysis the most powerful adversary is measured via a notion of approximate process equivalence. Even if finding the most powerful adversary is in general impractical, we show that this requires only a finite number of checks for a particular family of adversaries which are related to a probabilistic information flow property.

The parallel ‘Deutschland-Modell’ - A message-passing version for distributed memory computers

The parallel ‘Deutschland-Modell’ and its implementation on distributed memory parallel computers using the message-passing library PARMACS 6.0 is described. Performance results on a Cray T3D are given and the problem of dynamical load imbalances is addressed.     

Ready to preorder: The case of weak process semantics

Recently, Aceto, Fokkink and Ingólfsdóttir proposed an algorithm to turn any sound and ground-complete axiomatisation of any preorder listed in the linear time-branching time spectrum at least as coarse as the ready simulation preorder, into a sound and ground-complete axiomatisation of the corresponding equivalence—its kernel. Moreover, if the former axiomatisation is ω-complete, so is the latter. Subsequently, de Frutos Escrig, Gregorio Rodríguez and Palomino generalised this result, so that the algorithm is applicable to any preorder at least as coarse as the ready simulation preorder, provided it is initials preserving. The current paper shows that the same algorithm applies equally well to weak semantics: the proviso of initials preserving can be replaced by other conditions, such as weak initials preserving and satisfying the second τ-law. This makes it applicable to all 87 preorders surveyed in “the linear time-branching time spectrum II” that are at least as coarse as the ready simulation preorder. We also extend the scope of the algorithm to infinite processes, by adding recursion constants. As an application of both extensions, we provide a ground-complete axiomatisation of the CSP failures equivalence for BCCS processes with divergence.     

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.     

Reasoning about dynamically evolving process structures

We develop a Hoare-style proof system for reasoning about the behaviour of processes that interact via a dynamically evolving communication structure.     

Process algebra with guards: Combining Hoare logic with process algebra

We extend process algebra with guards, comparable to the guards in guarded commands or conditions in common programming constructs such as if — then — else — fi and while — do — od.The extended language is provided with an operational semantics based on transitions between pairs of a process and a (data-)state. The data-states are given by a data environment that also defines in which data-states guards hold and how atomic actions (non-deterministically) transform these states. The operational semantics is studied modulo strong bisimulation equivalence. For basic process algebra (without operators for parallelism) we present a small axiom system that is complete with respect to a general class of data environments. Given a particular data environmentL we add three axioms to this system, which is then again complete, provided weakest preconditions are expressible andL is sufficiently deterministic.Then we study process algebra with parallelism and guards. A two phase-calculus is provided that makes it possible to prove identities between parallel processes. Also this calculus is complete. In the last section we show that partial correctness formulas can easily be expressed in this setting. We use process algebra with guards to prove the soundness of a Hoare logic for linear processes by translating proofs in Hoare logic into proofs in process algebra.Supported by ESPRIT Basic Research Action no. 3006 (CONCUR) and by RACE project no. 1046 (SPECS).Supported by RACE project no. 1046 (SPECS).     

A multilevel parallel solver for block tridiagonal and banded linear systems

This paper describes an efficient algorithm for the parallel solution of systems of linear equations with a block tridiagonal coefficient matrix. The algorithm comprises a multilevel LU-factorization based on block cyclic reduction and a corresponding solution algorithm.

The paper includes a general presentation of the parallel multilevel LU-factorization and solution algorithms, but the main emphasis is on implementation principles for a message passing computer with hypercube topology. Problem partitioning, processor allocation and communication requirement are discussed for the general block tridiagonal algorithm.

Band matrices can be cast into block tridiagonal form, and this special but important problem is dealt with in detail. It is demonstrated how the efficiency of the general block tridiagonal multilevel algorithm can be improved by introducing the equivalent of two-way Gaussian elimination for the first and the last partitioning and by carefully balancing the load of the processors. The presentation of the multilevel band solver is accompanied by detailed complexity analyses.

The properties of the parallel band solver were evaluated by implementing the algorithm on an Intel iPSC hypercube parallel computer and solving a larger number of banded linear equations using 2 to 32 processors. The results of the evaluation include speed-up over a sequential processor, and the measure values are in good agreement with the theoretical values resulting from complexity analysis. It is found that the maximum asymptotic speed-up of the multilevel LU-factorization using p processors and load balancing is approximated well by the expression (p +6)/4.

Finally, the multilevel parallel solver is compared with solvers based on row and column interleaved organization.     

Efficient symbolic computation of process expressions

This paper describes three optimization techniques for the eb³ process algebra. The optimizations are expressed in a new deterministic operational semantics which is shown to be trace-equivalent to a traditional non-deterministic operational semantics. Internal action transitions are eliminated by an efficient preruntime analysis of the structure of a process expression. Execution environments are used to optimize variable instantiation using lazy evaluation. Non-determinism is eliminated by returning a choice between possible transitions. This new operational semantics is implemented in the eb³pai process algebra interpreter to support the eb³ method. The goal of this method is to automate the development of information systems using, among other mechanisms, efficient symbolic computation of process expressions.     

A note on an expressiveness hierarchy for multi-exit iteration

Multi-exit iteration is a generalization of the standard binary Kleene star operation. The addition of this construct to Basic Process Algebra (BPA) yields a more expressive language than that obtained by augmenting BPA with the standard binary Kleene star. This note offers an expressiveness hierarchy, modulo bisimulation equivalence, for the family of multi-exit iteration operators proposed by Bergstra, Bethke and Ponse.     

Process algebras for systems diagnosis

In this paper we propose a new characterization of model-based diagnosis based on process algebras, a framework which is widely used in several areas of computer science. We show that process algebras provide a powerful modelling language which allows us to capture, in an uniform way, different types of models of physical systems, including models of time-varying and dynamic behavior. Then we provide a characterization of diagnosis which is equivalent to the “classical” abductive one. This suggests new interesting opportunities for research on relations between model-based reasoning and process algebras.     

随机进程代数新技术综述

本文以PEPA语言为例,对近年来发展起来的随机进程代数的缓解状态空间爆炸问题的新技术做一个综述．     

Lambda: A Mathematica package for operator product expansions in vertex algebras

We give an introduction to the Mathematica package Lambda, designed for calculating λ-brackets in both vertex algebras, and in SUSY vertex algebras. This is equivalent to calculating operator product expansions in two-dimensional conformal field theory. The syntax of λ-brackets is reviewed, and some simple examples are shown, both in component notation, and in N=1 superfield notation.

Program summary

Program title: LambdaCatalogue identifier: AEHF_v1_0Program summary URL:http://cpc.cs.qub.ac.uk/summaries/AEHF_v1_0.htmlProgram obtainable from: CPC Program Library, Queen's University, Belfast, N. IrelandLicensing provisions: GNU General Public LicenseNo. of lines in distributed program, including test data, etc.: 18 087No. of bytes in distributed program, including test data, etc.: 131 812Distribution format: tar.gzProgramming language: MathematicaComputer: See specifications for running Mathematica V7 or above.Operating system: See specifications for running Mathematica V7 or above.RAM: Varies greatly depending on calculation to be performed.Classification: 4.2, 5, 11.1.Nature of problem: Calculate operator product expansions (OPEs) of composite fields in 2d conformal field theory.Solution method: Implementation of the algebraic formulation of OPEs given by vertex algebras, and especially by λ-brackets.Running time: Varies greatly depending on calculation requested. The example notebook provided takes about 3 s to run.     

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.     

A Probabilistic Scheduler for the Analysis of Cryptographic Protocols

When modelling cryto-protocols by means of process calculi which express both nondeterministic and probabilistic behavior, it is customary to view the scheduler as an intruder. It has been established that the traditional scheduler needs to be carefully calibrated in order to more accurately reflect the intruder's capabilities for controlling communication channels. We propose such a class of schedulers through a semantic variant called PPC_νσ, of the Probabilistic Poly-time Calculus (PPC) of Mitchell et al. [J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science, 353:118–164, 2006] and we illustrate the pertinence of our approach by an extensive study of the Dining Cryptographers (DCP) [David Chaum. The dining cryptographers problem: Unconditional sender and recipient untraceability. J. Cryptology, 1(1):65–75, 1988] protocol. Along these lines, we define a new characterization of Mitchell et al.'s observational equivalence [J.C. Mitchell, A. Ramanathan, A. Scedrov, and V. Teague. A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science, 353:118–164, 2006] more suited for taking into account any observable trace instead of just a single action as required in the analysis of the DCP.