Search

This paper is an attempt to integrate the algebra of communicating processes (ACP) and the algebra of flownomials (AF). Basically, this means to combine axiomatized parallel and looping operators. To this end we introduce a model of process graphs with multiple entries and exits. In this model the usual operations of both algebras are defined, e.g. alternative composition (this covers both the sum of ACP and the disjoint sum of AF), sequential composition, feedback, parallel composition, left merge, communication merge, encapsulation, etc. The main results consist of correct and complete axiomatisations of process graphs modulo isomorphism and modulo bisimulation.

We classify the computable and semicomputable algebras in terms of finite equational initial algebra specifications and their properties as term term rewriting systems, such as completeness. Further results on properties of these specifications, such as on their size and orthogonality, are provided which show that our main results are the best possible.

We consider a model of the real time process algebra of [1,2,3] based on the nonstandard reals. As a subalgebra, we obtain a theory in which the urgent actions of ATP, TiCCS, TeCCS can be modeled.

This paper is concerned with finding complete axiomatizations of probabilistic processes. We examine this problem within the context of the process algebra ACP and obtain as our endresult the axiom system pr ACP−l, a version of ACP whose main innovation is a probabilistic asynchronous interleaving operator. Our goal was to introduce probability into ACP in as simple a fashion as possible, Optimally, ACP should be the homomorphic image of the probabilistic version in which the probabilities are forgotten, We begin by weakening slightly ACP to obtain the axiom system ACP−l. The main difference between ACP and ACP−l is that the axiom x + δ = x, which does not yield a plausible interpretation in the generative model of probabilistic computation, is rejected in ACP−l. We argue that this does not affect the usefulness of ACP−l in practice, and show how ACP can be reconstructed from ACP−l with a minimal amount of technical machinery. pr ACP−l is obtained from ACP−l through the introduction of probabilistic alternative and parallel composition operators, and a process graph model for pr ACP−l based on probabilistic bisimulation is developed. We show that pr ACP−l is a sound and complete axiomatization of probabilistic bisimulation for finite processes, and that pr ACP−l can be homomorphically embedded in ACP−l as desired. Our results for ACP−l and pr ACP−l are presented in a modular fashion by first considering several subsets of the signatures, We conclude with a discussion about adding an iteration operator to pr ACP−l.

The axiom system ACP of [BEK84a] was extended to discrete time in [BAB95]. Here we proceed to define the silent step in this theory in branching bisimulation semantics [GLW91, BAW90] rather than weak bisimulation semantics [MIL89, BEK85]. 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.

We give here a simple proof of the fact that on transition systems bisimulation is the equivalence relation generated by simulation via functions. The proof entirely rests on simple rules of the calculus of relations.

The objective of this paper is to bridge the gap between ACP and TCSP. To this end, ACP is extended with two non-deterministic choice operators in a setting of bisimulation semantics. With these operators, we can express safety properties of systems without the use of silent steps, and we can verify safety properties in a setting in which no assumption on fairness (or unfairness) has been made.

In a flowchart scheme an atomic action is modelled as a vertex (box), while in a process graph an atomic action is modelled as an edge. We define translations between these two graphical representations. By using these translations, we show that the classical bisimulation equivalence on process graphs coincides with the natural extension of the classical step-bystep flowchart equivalence to the nondeterministic case. This result allows us to translate axiomatisation results from flowcharts to processes and viceversa.

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.

We study a non interleaving subalgebra of a reduct of a model of ACP. The model discussed uses step bisimulation semantics. We can derive identities in this model with the help of the (interleaving) ACP calculus with multi-actions. We study the connection with Petri nets, and introduce causalities and a causal state operator.

Several new operators are introduced on top of the algebra of communicating processes (ACP) from [BK 84] in order to incorporate stable signals in process algebra. Semantically this involves assigning labels to nodes of process graphs in addition to the actions that serve as labels of edges. The labels of nodes are called signals. In combination with the operators of BPA, two signal insertion operators allow to describe each finite tree labeled with actions and signals. In the context of parallel processes there is a new feature connected with signals: the signal observation mechanism. This mechanism is organised on basis of a signal observation function in very much the same way as the communication mechanism of ACP is organised around a communication function. Also, we discuss conditionals on signals and processes, and make much use of them in our examples.

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

A version of classical real space process algebra is given in which messages travel with constant speed through a three-dimensional medium. It follows that communication is asynchronous and has a broadcasting character. A state operator is used to describe asynchronous message transfer and a priority mechanism allows to express the broadcasting mechanism. As an application, a protocol is specified in which the receiver moves with respect to the sender.

We study a variety of ways to specify a two sorted structure involving the Booleans B, with constants true and false and a finite set D with an equality function eq to the Booleans, under the assumption that there is a constant (name) for each element of D. The specifications are evaluated with respect to several properties, like textual length, efficiency in execution and the use of special features.

The object 0 acts as a zero for both sum and multiplication in process algebra. The constant δ, representing deadlock or inaction, is only a left zero for multiplication. We will call 0 predictable failure.

Having concerned ourselves with boundedness properties of algebraic data structure specifications in the sense of the ADJ Group (see [4, 6, 7]) before now—see [1], which is in a sense a follow-up of [3] of Bergstra and Tucker—we show in this paper that data structures of cardinality > n can be specified by means of a bounded number of equations, not depending on n, which are each of length O(n) only

The following problem is investigated in the paper: what structures can be uniquely defined by algorithmic properties? The algorithmic properties are represented in this paper as open formulae of the logic of effective definitions. This approach can be viewed as an alternative way of defining abstract data types.

An unbounded queue over a finite set of data values is a process Q in A∞ defined by an infinite system of guarded equations. The aim of this paper is to show that no finite system of guarded equations is capable of defining Q.

An algebra is said to be iterative if every nontrivial finite system of fixed-point equations has unique solution. The paper discusses possibilities of finding topological structure for a given iterative algebra so that the unique solution of every system S can be approximated by a sequence of elements generated from S.

In [2] Jerzy Tiuryn has introduced Logic of Effective Definitions (LED) in which properties of effective definitional schemes are expressed. With respect to the quantifier-free part of it, he proved that each open formula is equivalent to one in a special conjunctive normal form. We prove that there is no finite bound to the number of conjuncts required for these normal forms.

The following fundamental theorem about the adequacy of the algebraic specification methods for data abstractions is proved. Let A be a data type with n subtypes. Then A is computable if, and only if, A possesses an equational specification, involving at most 3( n + 1) hidden operators and 2( n + 1) axioms, which defines it under initial and final algebra semantics simultaneously.

A mechanism is introduced to describe priorities in ACP, the algebra of communicating processes, whereby some actions have priority over others in a non-deterministic choice (or sum). This mechanism can be used to model the working of interrupts in a distributed system. This is illustrated in an extensive example.

A general definition of a process is given. Recursive processes and relative recursion for processes are defined and the degree theory of processes is studied. We construct a process of minimal degree

In [5] it has been proved that by using hidden functions the number of equations needed to specify a finite data type is bounded by numbers depending only on the signature of that data type. In the special case of a finite minimal unoid, however, it seems to be relevant to ask whether or not a specification can also be made by a bounded number of equations using only unary hidden functions. In this paper we prove that this can be done.

Summary § 1 is concerned with the term model of the α-calculus. It is proved that Church's δ is not dofinable and that the definable functions into the numerals are constant. In § 2 it is proved that for several α-algebras the range of a representable function is either a singleton or infinite. In § 3 it is examined in which α-algebras the local representability of external functions implies the global representability.

A 0-totalised field is a field in which division is a total operation with 0(−1)=0. Equational reasoning in such fields is greatly simplified but in deriving a term one still wishes to know whether or not the calculation has invoked 0(−1). If it has not then we call the derivation division safe. We propose three methods of guaranteeing division safe calculations in 0-totalised fields.

In a previous paper we developed an algebraic theory about threads and a form of concurrency where some deterministic interleaving strategy determines how threads that exist concurrently are interleaved. The interleaving of different threads constitutes a multi-thread. Several multi-threads may exist concurrently on a single host in a network, several host behaviours may exist concurrently in a single network on the internet, etc. In the current paper we assume that the above-mentioned kind of interleaving is also present at those other levels. We extend the theory developed so far with features to cover the multi-level case. We employ the resulting theory to develop a simplified, formal representation schema of the design of systems that consist of several multi-threaded programs on various hosts in different networks and to verify a property of all systems designed according to that schema.

Threads as considered in basic thread algebra are primarily looked upon as behaviours exhibited by sequential programs on execution. It is a fact of life that sequential programs are often fragmented. Consequently, fragmented program behaviours are frequently found. In this paper, we consider this phenomenon. We extend basic thread algebra with the barest mechanism for sequencing of threads that are taken for fragments. This mechanism, called poly-threading, supports both autonomous and non-autonomous thread selection in sequencing. We relate the resulting theory to the algebraic theory of processes known as ACP and use it to describe analytic execution architectures suited for fragmented programs. We also consider the case where the steps of fragmented program behaviours are interleaved in the ways of non-distributed and distributed multi-threading., Comment: 24 pages, sections 9, 10, and 11 are added

We study the notion of bisimulation between process graphs with silent or invisible steps (τ-steps). This leads to a normalisation or minimalisation result for regular processes with τ-steps and subject to operations + (alternative composition), · (sequential composition) and ∥ (parallel composition or free merge), thereby answering a question of MTLNER [10] and proving the consistency of a version of Koomen's fair abstraction rule.

We consider two ways of assigning semantics to a class of statements built from a set of atomic actions (the ‘alphabet‘), by means of sequential composition, nondeterministic choice, recursion and merge (arbitrary interleaving). The first is linear time semantics (LT), stated in terms of trace theory; the semantic domain is the collection of all closed sets of finite and infinite words. The second is branching time semantics (BT), as introduced by de Bakker and Zucker; here the semantic domain is the metric completion of the collection of finite processes. For LT we prove the continuity of the operations (merge, sequential composition) in a direct, combinatorial way.

In this paper a process is viewed as a labeled graph modulo bisimulation equivalence. Three topics are covered: (i) specification of processes using finite systems of equations over the syntax of process algebra; (ii) inference systems which are complete for proving the equivalence of regular (finite state) processes; (iii) variations of the bisimulation model.

A context-free grammar (CFG) in Greibach Normal Form coincides, in another notation, with a system of guarded recursion equations in Basic Process algebra. Hence, to each CFG, aprocess can be assigned absolution, which has as its set of finite traces the context-free language (CFL)determined by that CFG. Although the equality problem for CFLs is unsolvable, the equality problem for the processes determined by CFGS turns out to be solvable. Here, equality on processes is given by a model of process graphs modulo bisimulation equivalence. The proof is given by displaying a periodic structure of the process graphs determined by CFG’S. As a corollary of the periodicity, a short proof of the solvability of the equivalence problem for simple context-free languages is given.

We discuss a data type specification language DSL(?) which is obtained from the first order language L(?) for a given signature ? by augmenting it with schemes. A specification is a pair (?, $$\mathbb{F}$$ ) with $$\mathbb{F}$$ a finite set of axioms in DSL(?). As semantics of such specifications we propose: standard model semantics, SMS. We investigate DSL/SMS as a specification mechanism for data types and compare it with both first order and algebraic specifications. A concise theory of parametrized data types is developed in this context.

We investigate the defining power of finite recursive specifications over the theory with + (alternative composition) and · (sequential composition) and λ (the state operator) over a finite set of states, and find that it is greater than that of the same theory without state operator. Thus, adding the state operator is an essential extension of BPA (the theory of processes over +, ·). On the other hand, applying the state operator to a regular process again gives a regular process. As a limiting result in the other direction, we find that not all PA-processes (where also parallel composition λ is present) can be defined over BPA plus state operator.

Renaming operators are introduced in concrete process algebra (concrete means that abstraction and silent moves are not considered). Examples of renaming operators are given: encapsulation, pre-abstraction, and localization. The authors show that renamings enhance the defining power of concrete process algebra by using the example of a queue. They give a definition of the trace set of a process, see when equality of trace sets implies equality of processes, and use trace sets to define the restriction of a process. Finally, they describe processes with actions that have a side effect on a state space and show how to use this for a translation of computer programs into process algebra

Formalizing informal requirements some aspects.- ViewPoint oriented software development: Methods and viewpoints in requirements engineering.- Using transformations to verify parallel programs.- Experiences with combining formalisms in VVSL.- A meta-environment for generating programming environments.- Introducing formal requirements into industry.- Where can I get gas round here? - an application of a design methodology for distributed systems.- Transformations of designs.- Norman's database modularised in COLD-K.- POLAR a picture-oriented language for abstract representations.- Inheritance in COLD.- A process specification formalism based on static COLD.- Specification of the transit node in PSFd.- Design of a specification language by abstract syntax engineering.- From an ERAE requirements specification to a PLUSS algebraic specification: A case study.

Publisher Summary One may give an alternative definition of C (the continuous functionals) as the functionals that express the fact that C is the maximal type-structure that does not lead to discontinuities. Then, one solves a problem using arguments from recursion theory on the continuous functionals. REC is the class of recursive functionals and RC is the class of recursively countable functionals. An unsatisfactory aspect from the computational point of view are the ψ­. A definition of the continuous functionals can be framed that uses as only topological notion the continuity of a functional. Further, one uses a notion of relative definability that is introduced by means of a typed.

We present an axiom system ACP, for communicating processes with silent actions (‘τ-steps’). The system is an extension of ACP, Algebra of Communicating Processes, with Milner's τ-laws and an explicit abstraction operator. By means of a model of finite acyclic process graphs for ACPτ, syntactic properties such as consistency and conservativity over ACP are proved. Furthermore, the Expansion Theorem for ACP is shown to carry over to ACPτ. Finally, termination of rewriting terms according to the ACPτ, axioms is probed using the method of recursive path orderings.

A programming system is a language made from a fixed class of data abstractions and a selection of familiar deterministic control and assignment constructs. It is shown that the sets of all ‘before-after’ first-order assertions which are true of programs in any such language can uniquely determine the input-output semantics of the language providing one allows the use of auxiliary operators on its ground types. After this, we study programming systems wherein the data types are syntactically defined using a first-order specification language with the objective of eliminating these auxiliary operators. Especial attention is paid to algebraic specifications, complete first-order specifications; and to arithmetical computation in the context of a specified programming system.