J.A. Bergstra

TCS Journal 2020 Journal Article

On the complexity of the correctness problem for non-zeroness test instruction sequences

• J.A. Bergstra
• C.A. Middelburg

This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each n > 0, each function from { 0, 1 } n to { 0, 1 } can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to { 0, 1 } n of the function from { 0, 1 } ⁎ to { 0, 1 } that models the non-zeroness test function, for n > 0, under several restrictions on the arbitrary instruction sequence.

I&C Journal 2010 Journal Article

A thread calculus with molecular dynamics

• J.A. Bergstra
• C.A. Middelburg

We present a theory of threads, interleaving of threads, and interaction between threads and services with features of molecular dynamics, a model of computation that bears on computations in which dynamic data structures are involved. Threads can interact with services of which the states consist of structured data objects and computations take place by means of actions which may change the structure of the data objects. The features introduced include restriction of the scope of names used in threads to refer to data objects. Because that feature makes it troublesome to provide a model based on structural operational semantics and bisimulation, we construct a projective limit model for the theory.

TCS Journal 2009 Journal Article

Meadows and the equational specification of division

• J.A. Bergstra
• Y. Hirshfeld
• J.V. Tucker

The rational, real and complex numbers with their standard operations, including division, are partial algebras specified by the axiomatic concept of a field. Since the class of fields cannot be defined by equations, the theory of equational specifications of data types cannot use field theory in applications to number systems based upon rational, real and complex numbers. We study a new axiomatic concept for number systems with division that uses only equations: a meadow is a commutative ring with a total inverse operator satisfying two equations which imply 0−1=0. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms for inverse, we start the development of a theory of meadows. We give a general representation theorem for meadows and find, as a corollary, that the conditional equational theory of meadows coincides with the conditional equational theory of zero totalized fields. We also prove representation results for meadows of finite characteristic.

I&C Journal 2006 Journal Article

Splitting bisimulations and retrospective conditions

• J.A. Bergstra
• C.A. Middelburg

We investigate conditional expressions in the setting of ACP, an algebraic theory about processes. We introduce ACPc, an extension of ACP with conditional expressions in which the conditions are taken from a free Boolean algebra over a set of generators, and also its main models, called full splitting bisimilation models. We add two simple mechanisms for condition evaluation to ACPc; and we show their connection with state operators and signal emission, mechanisms from other extensions of ACP usable for condition evaluation. To allow for looking back on conditions under which preceding actions have been performed, we add a retrospection operator on conditions to ACPc. The choice of conditions forces us to introduce a new variant of bisimulation. However, without the generality implied by that choice, it would not have been possible to extend ACPc with retrospection. The addition of retrospection is a basic way to increase expressiveness.

TCS Journal 2005 Journal Article

Polarized process algebra with reactive composition

• J.A. Bergstra
• I. Bethke

Polarized processes are introduced to model the asymmetric interaction of systems. The asymmetry stems from the distinction between service and request. The scheduled concurrent composition of two polarized processes is called client–server composition or reactive composition, placing one process in the role of a client and the other process in the role of a server which is supposed to react on requests. The technical goal of this paper is to provide a definition of reactive composition for polarized processes and to prove that reactive composition thus defined is associative.

TCS Journal 2005 Journal Article

Process algebra for hybrid systems

• J.A. Bergstra
• C.A. Middelburg

We propose a process algebra obtained by extending a combination of the process algebra with continuous relative timing from Baeten and Middelburg (Process Algebra with Timing, Springer, Berlin, 2002, Chapter 4), and the process algebra with propositional signals from Baeten and Bergstra (Theoret. Comput. Sci. 177 (1977) 381–405). The proposed process algebra makes it possible to deal with the behaviour of hybrid systems, i. e. systems in which the instantaneous state transitions caused by performing actions are alternated with continuous state evolutions. This process algebra has, in addition to equational axioms, rules to derive equations with the help of real analysis.

TCS Journal 1997 Journal Article

Process algebra with prepositional signals

• J.C.M. Baeten
• J.A. Bergstra

We consider processes that have transitions labeled with atomic actions, and states labeled with formulas over a propositional logic. These state labels are called signals. A process in a parallel composition may proceed conditionally, dependent on the presence of a signal in the process in parallel. This allows a natural treatment of signal observation.

I&C Journal 1995 Journal Article

Axiomatizing Probabilistic Processes: ACP with Generative Probabilities

• J.C.M. Baeten
• J.A. Bergstra
• S.A. Smolka

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.

I&C Journal 1995 Journal Article

Homomorphism Preserving Algebraic Specifications Require Hidden Sorts

• J.A. Bergstra
• J. Heering

Although every computable data type has an initial algebra specification with hidden functions, it may happen that some of the homomorphic images of the data type are not models of the specification. The latter are reducts of algebras that would be models of the specification if all its functions were visible, whereas the homomorphic images of the data type are independent of the specification and need not be compatible with the hidden functions used in it. A hidden function specification that does not exclude any of the homomorphic images of its initial model from its model class will be called homomorphism preserving. It turns out that, unlike unrestricted initial homomorphism preserving. It turns out that, unlike unrestricted initial algebra specification, homomorphism preserving initial algebra specification of computable data types requires both hidden sorts and hidden functions.

TCS Journal 1994 Journal Article

Which data types have ω-complete initial algebra specifications?

• J.A. Bergstra
• J. Heering

An algebraic specification is called ω-complete or inductively complete if all (open as well as closed) equations valid in its initial model are equationally derivable from it, i. e. , if the equational theory of the initial model is identical to the equational theory of the specification. As the latter is recursively enumerable, the initial model of an ω-complete algebraic specification is a data type with a recursively enumerable equational theory. We show that if hidden sorts and functions are allowed in the specification, the converse is also true: every data type with a recursively enumerable equational theory has an ω-complete initial algebra specification with hidden sorts and functions. We also show that in the case of finite data types the hidden sorts can be dispensed with.

TCS Journal 1991 Journal Article

Recursive process definitions with the state operator

• J.C.M. Baeten
• J.A. Bergstra

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.

TCS Journal 1989 Journal Article

Term-rewriting systems with rule priorities

• J.C.M. Baeten
• J.A. Bergstra
• J.W. Klop
• W.P. Weijland

In this paper we discuss term-rewriting systems with rule priorities, which simply is a partial ordering on the rules. The procedural meaning of such an ordering then is, that the application of a rule of lower priority is allowed only if no rule of higher priority is applicable. The semantics of such a system is discussed. It turns out that the class of all bounded systems indeed has such a semantics.

I&C Journal 1988 Journal Article

Global renaming operators in concrete process algebra

• J.C.M. Baeten
• J.A. Bergstra

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. We show that renamings enhance the defining power of concrete process algebra by using the example of a queue. We 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, we 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.

TCS Journal 1987 Journal Article

Algebraic specifications of computable and semicomputable data types

• J.A. Bergstra
• J.V. Tucker

An extensive survey is given of the properties of various specification mechanisms based on initial algebra semantics.

TCS Journal 1987 Journal Article

On the consistency of Koomen's Fair Abstraction Rule

• J.C.M. Baeten
• J.A. Bergstra
• J.W. Klop

We construct a graph model for ACPτ, the algebra of communicating processes with silent steps, in which Koomen's Fair Abstraction Rule (KFAR) holds, and also versions of the Approximation Induction Principle (AIP) and the Recursive Definition & Specification Principles (RDP&RSP). We use this model to prove that in ACPT (but not in ACP!) each computably recursively definable process is finitely recursively definable.

TCS Journal 1985 Journal Article

Algebra of communicating processes with abstraction

• J.A. Bergstra
• J.W. Klop

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.

TCS Journal 1984 Journal Article

Linear time and branching time semantics for recursion with merge

• J.W. de Bakker
• J.A. Bergstra
• J.W. Klop
• J.-J.Ch. Meyer

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. Next, a connection between LT and BT is established by means of the operation trace which assigns to a process its set of traces. We show that the trace set of a process is closed and that trace is continuous. This requires the compactness of the semantic domains, ensured by the finiteness of the alphabet. Using trace, we then can carry over BT into LT.

TCS Journal 1984 Journal Article

Proving program inclusion using Hoare's logic

• J.A. Bergstra
• J.W. Klop

We explore conservative refinements of specifications. These form a quite appropriate framework for a proof theory for program inclusion based on a proof theory for program correctness. We propose two formalized proof methods for program inclusion and prove these to be sound. Both methods are incomplete but seem to cover most natural cases.

TCS Journal 1983 Journal Article

Hoare's logic and Peano's arithmetic

• J.A. Bergstra
• J.V. Tucker

We develop the proof theory of Hoare's logic for the partial correctness of while- programs applied to arithmetic as it is defined by Peano's axioms. By representing the strongest postcondition calculus in Peano arithmetic PA, we are able to show that Hoare's logic over PA is equivalent to PA itself.

TCS Journal 1983 Journal Article

Hoare's logic for programming languages with two data types

• J.A. Bergstra
• J.V. Tucker

We consider the completeness of Hoare's logic with a first-order assertion language applied to while-programs containing variables of two (or more) distinct types. Whilst Cook's completeness theorem generalizes to many-sorted interpretations, certain fundamentally important structures turn out not to be expressive. We study the case of programs with distinguished counter variables and Boolean variables adjoined; for example, we show that adding counters to arithmetic destroys expressiveness.

TCS Journal 1982 Journal Article

Floyd's principle, correctness theories and program equivalence

• J.A. Bergstra
• J. Tiuryn
• J.V. Tucker

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.

TCS Journal 1982 Journal Article

On the elimination of iteration quantifiers in a fragment of algorithmic logic

• J.A. Bergstra
• J.-J.Ch. Meyer

In this paper we study the elimination of the iteration quantifier ∪ in a special set of algorithmic formulae. Something similar has been done by G. Mirkowska and E. Orlowska by means of a system of procedures. We, however, show that elimination is already possible by using the programs in our sublanguage itself.

TCS Journal 1982 Journal Article

Some natural structures which fail to possess a sound and decidable hoare-like logic for their while-programs

• J.A. Bergstra
• J.V. Tucker