Functional units for natural numbers (2009)
Bergstra, J. A., Middelburg, C. A.
Interaction with services provided by an execution environment forms part of the behaviours exhibited by instruction sequences under execution. Mechanisms related to the kind of interaction in...
Instruction sequence processing operators (2009)
Bergstra, J. A., Middelburg, C. A.
This paper concerns instruction sequences whose execution involves the processing of instructions by an execution environment that offers a family of services and may yield a Boolean value at...
Partial Komori fields and imperative Komori fields (2009)
Bergstra, J. A., Middelburg, C. A.
This paper is concerned with the status of 1/0 and ways to deal with it. These matters are treated in the setting of Komori fields, also known as non-trivial cancellation meadows. Different...
Bergstra, J. A., Middelburg, C. A.
An inversive meadow is a commutative ring with identity equipped with a multiplicative inverse operation made total by choosing 0 as its value at 0. Previously, inversive meadows were shortly called...
Indirect jumps improve instruction sequence performance (2009)
Bergstra, J. A., Middelburg, C. A.
Instruction sequences with direct and indirect jump instructions are as expressive as instruction sequences with direct jump instructions only. We show that, in the case where the number of...
Inversive Meadows and Divisive Meadows (2009)
Bergstra, J. A., Middelburg, C. A.
An inversive meadow is a commutative ring with identity and a total multiplicative inverse operation whose value at 0 is 0. Previously, inversive meadows were shortly called meadows. In this paper,...
Instruction sequence notations with probabilistic instructions (2009)
Bergstra, J. A., Middelburg, C. A.
This paper concerns probabilistic instruction sequences. We use the term probabilistic instruction sequence for an instruction sequence that contains probabilistic instructions, i.e. instructions...
A protocol for instruction stream processing (2009)
Bergstra, J. A., Middelburg, C. A.
The behaviour produced by an instruction sequence under execution is a behaviour to be controlled by some execution environment: each step performed actuates the processing of an instruction by the...
A process calculus with finitary comprehended terms (2009)
Bergstra, J. A., Middelburg, C. A.
Meadow enriched ACP process algebras are essentially enrichments of models of the axiom system ACP that concern processes in which data are involved, the mathematical structure of data being a...
Transmission protocols for instruction streams (2009)
Bergstra, J. A., Middelburg, C. A.
Threads as considered in thread algebra model behaviours to be controlled by some execution environment: upon each action performed by a thread, a reply from its execution environment -- which takes...
Timed tuplix calculus and the Wesseling and van den Berg equation (2009)
Bergstra, J. A., Middelburg, C. A.
We formalize a cumulative interest compliant conservation requirement for pure financial products proposed by Wesseling and van den Bergh to make financial issues relating to these products amenable...
Meadow enriched ACP process algebras (2009)
Bergstra, J. A., Middelburg, C. A.
We introduce the notion of an ACP process algebra. The models of the axiom system ACP are the origin of this notion. ACP process algebras have to do with processes in which no data are involved. We...
Bergstra, J. A., Hirshfeld, Y., Tucker, J. V.
A skew meadow is a non-commutative ring with an inverse operator satisfying two special equations and in which the inverse of zero is zero. All skew fields and products of skew fields can be viewed...
Meadows and the equational specification of division (2009)
Bergstra, J. A., Hirshfeld, Y., Tucker, J. V.
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...
On the expressiveness of single-pass instruction sequences (2009)
Bergstra, J.A., Middelburg, C.A.
We perceive programs as single-pass instruction sequences. A single-pass instruction sequence under execution is considered to produce a behaviour to be controlled by some execution environment....
Thread extraction for polyadic instruction sequences (2009)
Bergstra, J.A., Middelburg, C.A.
Instruction sequences are often fragmented. An important reason for instruction sequence fragmentation is that the execution architecture at hand to execute instruction sequences sets bounds to the...
The State Operator in Real Time Process Algebra (2008)
Abstract: We extend the real time process algebra of [BB91a] with the state operator of [BB88]. We show the usefulness of this extension in several examples. We use concepts from (classical) real...
Instruction sequences for the production of processes (2008)
Bergstra, J. A., Middelburg, C. A.
Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours:...
On the expressiveness of single-pass instruction sequences (2008)
Bergstra, J. A., Middelburg, C. A.
We perceive programs as single-pass instruction sequences. A single-pass instruction sequence under execution is considered to produce a behaviour to be controlled by some execution environment....
Instruction sequences and non-uniform complexity theory (2008)
Bergstra, J. A., Middelburg, C. A.
We develop theory concerning non-uniform complexity in a setting in which the notion of single-pass instruction sequence considered in program algebra is the central notion. We define counterparts of...
J A Bergstra, Y Hirschfeld, J V Tucker
A meadow is a commutative ring with an inverse operator satisfying two equations and in which 0 −1 = 0. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms...
Proposition Algebra with Projective Limits (2008)
Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a proposition, atomic propositions may yield different...
Data linkage dynamics with shedding (2008)
Bergstra, J. A., Middelburg, C. A.
We study shedding in the setting of data linkage dynamics, a simple model of computation that bears on the use of dynamic data structures in programming. Shedding is complementary to garbage...
Tuplix Calculus Specifications of Financial Transfer Networks (2008)
Bergstra, J. A., Trenite, S. Nolst, Van Der Zwaag, M. B.
We study the application of Tuplix Calculus in modular financial budget design. We formalize organizational structure using financial transfer networks. We consider the notion of flux of money over a...
Data linkage algebra, data linkage dynamics, and priority rewriting (2008)
Bergstra, J. A., Middelburg, C. A.
We introduce an algebra of data linkages. Data linkages are intended for modelling the states of computations in which dynamic data structures are involved. We present a simple model of computation...
A Thread Calculus with Molecular Dynamics ⋆ (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. In a previous paper, we developed an algebraic theory of threads, interleaving of threads, and interaction between threads and services. In the current paper, we extend that theory with...
J A Bergstra, J V Tucker, J A Bergstra, Singleton Park
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...
Process Algebra with Conditionals in the Presence of Epsilon (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. In a previous paper, we presented several extensions of ACP with conditional expressions, including one with a retrospection operator on conditions to allow for looking back on conditions...
Bounded Stacks, Bags and Queues (2008)
Abstract. We prove that a bounded stack can be specified in process algebra with just the operators alternative and sequential composition and iteration. The bounded bag cannot be specified with...
Splitting bisimulations and retrospective conditions (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. We investigate conditions in the setting of the algebraic theory about processes known as ACP. We present ACP c, an extension of ACP with guarded commands, and its main models, called its...
Summary. 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...
Machine Structure Oriented Control Code Logic ⋆ (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. Control code is a concept that is closely related to a frequently occurring practitioner’s view on what is a program: code that is capable of controlling the behaviour of some machine. We...
IOS Press Located Actions in Process Algebra with Timing (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. We propose a process algebra obtained by adapting the process algebra with continuous relative timing from Baeten and Middelburg [Process Algebra with Timing, Springer, 2002, Chap. 4] to...
ALGEBRAIC TOOLS FOP. SYSTEM CONSTRUCTION (2008)
Computer systems, in all their diversity, often share certain common properties: they are hierarchically organised into levels of abstraction and, at each level, they pos-sess a certain architecture...
Preferential Choice and Coordination Conditions (2008)
J. A. Bergstra, C. A. Middelburg
Abstract. We present a process algebra with conditional expressions of which the conditions concern the enabledness of actions in the context in which a process is placed. With those conditions, it...
of Computing Real Space Process Algebra (2008)
Abstract. 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...
Thread algebra for poly-threading (2008)
Bergstra, J. A., Middelburg, C. A.
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...
Thread extraction for polyadic instruction sequences (2008)
Bergstra, J. A., Middelburg, C. A.
Instruction sequences are often fragmented. An important reason for instruction sequence fragmentation is that the execution architecture at hand to execute instruction sequences sets bounds to the...
Programming an interpreter using molecular dynamics (2008)
Bergstra, J. A., Middelburg, C. A.
PGA (ProGram Algebra) is an algebra of programs which concerns programs in their simplest form: sequences of instructions. Molecular dynamics is a simple model of computation developed in the setting...
We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We...
An instruction sequence semigroup with repeaters (2008)
In the setting of program algebra (PGA) we consider the repeat instruction. This special instruction was designed to represent infinite sequences of primitive instructions as finite, linear programs....
A generic basis theorem for cancellation meadows (2008)
Let Q_0 denote the rational numbers expanded to a “meadow'', that is, after taking its zero-totalized form (0^{-1}=0) as the preferred interpretation. In this paper we consider “cancellation...
Mechanistic behavior of single-pass instruction sequences (2008)
Earlier work on program and thread algebra detailed the functional, observable behavior of programs under execution. In this article we add the modeling of unobservable, mechanistic processing, in...
A meadow is a zero totalised field (0^{-1}=0), and a cancellation meadow is a meadow without proper zero divisors. In this paper we consider differential meadows, i.e., meadows equipped with...
Towards a formalization of budgets (2008)
Bergstra, J.A., Nolst Trenité, S.
We go into the need for, and the requirements on, a formal theory of budgets. We present a simple algebraic theory of rational budgets, i.e., budgets in which amounts of money are specified by...
Proposition algebra with projective limits (2008)
Sequential propositional logic deviates from ordinary propositional logic by taking into account that during the sequential evaluation of a proposition, atomic propositions may yield different...
Instruction sequences and non-uniform complexity theory (2008)
Bergstra, J.A., Middelburg, C.A.
We develop theory concerning non-uniform complexity in a setting in which the notion of single-pass instruction sequence considered in program algebra is the central notion. We define counterparts of...
Thread algebra for poly-threading (2008)
Bergstra, J.A., Middelburg, C.A.
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...
Instruction sequences for the production of processes (2008)
Bergstra, J.A., Middelburg, C.A.
Single-pass instruction sequences under execution are considered to produce behaviours to be controlled by some execution environment. Threads as considered in thread algebra model such behaviours:...
Data linkage algebra, data linkage dynamics, and priority rewriting (2008)
Bergstra, J.A., Middelburg, C.A.
We introduce an algebra of data linkages. Data linkages are intended for modelling the states of computations in which dynamic data structures are involved. We present a simple model of computation...
Data linkage dynamics with shedding (2008)
Bergstra, J.A., Middelburg, C.A.
We study shedding in the setting of data linkage dynamics, a simple model of computation that bears on the use of dynamic data structures in programming. Shedding is complementary to garbage...
Program algebra with a jump-shift instruction (2008)
Bergstra, J.A., Middelburg, C.A.
We study sequential programs that are instruction sequences with jump-shift instructions in the setting of PGA (ProGram Algebra). Jump-shift instructions preceding a jump instruction increase the...
Parallel processes with implicit computational capital (2008)
Bergstra, J.A., Middelburg, C.A.
We propose a process algebra which is concerned with processes that have an implicit computational capital. This process algebra is intended to be helpful when designing computer-based systems of...
Maurer computers for pipelined instruction processing (2008)
Bergstra, J.A., Middelburg, C.A.
We model micro-architectures with non-pipelined instruction processing and pipelined instruction processing using Maurer machines, basic thread algebra and program algebra. We show that stored...
Simulating Turing machines on Maurer machines (2008)
Bergstra, J.A., Middelburg, C.A.
In a previous paper, we used Maurer machines to model and analyse micro-architectures. In the current paper, we investigate the connections between Turing machines and Maurer machines with the...
Tuplix Calculus specifications of financial transfer networks (2008)
Bergstra, J.A., Nolst Trenité, S.
We study the application of Tuplix Calculus in modular financial budget design. We formalize organizational structure using financial transfer networks. We consider the notion of flux of money over a...
Distributed strategic interleaving with load balancing (2008)
Bergstra, J.A., Middelburg, C.A.
In a previous paper, we developed an algebraic theory of threads, interleaving of threads, and interaction of threads with services. In the current paper, we assume that the threads and services are...
Division safe calculation in totalised fields (2008)
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...
The Software Invention Cube: A classification scheme for software inventions (2008)
The patent system protects inventions. The requirement that a software invention should make ‘a technical contribution’ turns out to be untenable in practice and this raises the question, what...
We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We...
Bergstra, J. A., Ponse, A., Van Der Zwaag, M. B.
We introduce a calculus for tuplices, which are expressions that generalize matrices and vectors. Tuplices have an underlying data type for quantities that are taken from a zero-totalized field. We...
Program algebra with a jump-shift instruction (2007)
Bergstra, J. A., Middelburg, C. A.
We study sequential programs that are instruction sequences with jump-shift instructions in the setting of PGA (ProGram Algebra). Jump-shift instructions preceding a jump instruction increase the...
Instruction sequences with dynamically instantiated instructions (2007)
Bergstra, J. A., Middelburg, C. A.
We study sequential programs that are instruction sequences with dynamically instantiated instructions. We define the meaning of such programs in two different ways. In either case, we give a...
Bounded Stacks, Bags and Queues (2007)
. We prove that a bounded stack can be specified in process algebra with just the operators alternative and sequential composition and iteration. The bounded bag cannot be specified with these...
Discrete-time Process Algebra and the Semantics of SDL (2007)
J. A. Bergstra, C. A. Middelburg, Y. S. Usenko
development of high integrity computing systems, (ii) highest level post-graduate university teaching, (iii) international level research, and, through the above, (iv) use of as sophisticated...
The axiom system ACP of [10] was extended to discrete time in [6]. Here, we proceed to define the silent step in this theory in branching bisimulation semantics [7, 15] rather than weak bisimulation...
Abstract. This paper is an attempt to integrate the algebra of communicating processes (ACP) and the algebra of ownomials (AF). Basically, this means to combine axiomatized parallel and looping...
Branching Time and Orthogonal Bisimulation Equivalence (2007)
J. A. Bergstra, A. Ponse, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Instruction sequences with indirect jumps (2007)
Bergstra, J. A., Middelburg, C. A.
We study sequential programs that are instruction sequences with direct and indirect jump instructions. The intuition is that indirect jump instructions are jump instructions where the position of...
An interface group for process components (2007)
Bergstra, J. A., Middelburg, C. A.
We take a process component as a pair of an interface and a behaviour. We study the composition of interacting process components in the setting of process algebra. We formalize the interfaces of...
Machine structure oriented control code logic (2007)
Bergstra, J. A., Middelburg, C. A.
Control code is a concept that is closely related to a frequently occurring practitioner's view on what is a program: code that is capable of controlling the behaviour of some machine. We present a...
On the operating unit size of load/store architectures (2007)
Bergstra, J. A., Middelburg, C. A.
We introduce a strict version of the concept of a load/store instruction set architecture in the setting of Maurer machines. We take the view that transformations on the states of a Maurer machine...
A thread calculus with molecular dynamics (2007)
Bergstra, J. A., Middelburg, C. A.
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...
About “trivial” software patents: The IsNot case (2007)
So-called “trivial” software patents undermine the patenting system and are detrimental for innovation. In this paper we use a case-based approach to get a better understanding of this...
Decision problems for pushdown threads (2007)
Bergstra, J.A., Bethke, I., Ponse, A.
Threads as contained in a thread algebra emerge from the behavioral abstraction from programs in an appropriate program algebra. Threads may make use of services such as stacks, and a thread using a...
Execution architectures for program algebra (2007)
We investigate the notion of an execution architecture in the setting of the program algebra PGA, and distinguish two sorts of these: analytic architectures, designed for the purpose of explanation...
The Rational Numbers as an Abstract Data Type (2007)
We give an equational specification of the field operations on the rational numbers under initial algebra semantics using just total field operations and 12 equations. A consequence of this...
Instruction Sequences with Indirect Jumps (2007)
J.A. Bergstra, C.A. Middelburg
We study sequential programs that are instruction sequences with direct and indirect jump instructions. The intuition is that indirect jump instructions are jump instructions where the position of...
Programming an Interpreter Using Molecular Dynamics (2007)
J.A. Bergstra, C.A. Middelburg
PGA (ProGram Algebra) is an algebra of programs which concerns programs in their simplest form: sequences of instructions. Molecular dynamics is a simple model of computation developed in the setting...
An Interface Group for Process Components ⋆ (2007)
J. A. Bergstra, C. A. Middelburg, J. A. Bergstra, C. A. Middelburg, J. A. Bergstra, C. A. Middelburg
Abstract. We take a process component as a pair of an interface and a behaviour. We study the composition of interacting process components in the setting of process algebra. We formalize the...
Instruction sequences with indirect jumps (2007)
J. A. Bergstra, J. A. Bergstra, J. A. Bergstra, C. A. Middelburg, C. A. Middelburg, C. A. Middelburg
Abstract. We study sequential programs that are instruction sequences with direct and indirect jump instructions. The intuition is that indirect jump instructions are jump instructions where the...
On the Operating Unit Size of Load/Store Arc hitectures, Programming Research Group (2007)
J. A. Bergstra, C. A. Middelburg
Abstract. We introduce a strict version of the concept of a load/store instruction set architecture in the setting of Maurer machines. We take the view that transformations on the states of a Maurer...
J A Bergstra, Y Hirschfeld, J V Tucker
A meadow is a commutative ring with an inverse operator satisfying two equations and in which 0 −1 = 0. All fields and products of fields can be viewed as meadows. After reviewing alternate axioms...
Towards a Formalization of Budgets (2007)
J. A. Bergstra, S. Nolst Trenite, J. A. Bergstra, S. Nolst Trenite, ...
We go into the need for, and the requirements on, a formal theory of budgets. We present a simple algebraic theory of rational budgets, i.e., budgets in which amounts of money are specified by...
Programming an interpreter using molecular dynamics (2007)
Bergstra, J.A., Middelburg, C.A.
PGA (ProGram Algebra) is an algebra of programs which concerns programs in their simplest form: sequences of instructions. Molecular dynamics is a simple model of computation developed in the setting...
Continuity Controlled Hybrid Automata (2006)
J. A. Bergstra, C. A. Middelburg
Abstract. We investigate the connections between the process algebra for hybrid systems of Bergstra and Middelburg and the formalism of hybrid automata of Henzinger et al. We give interpretations of...
Thread Algebra for Strategic Interleaving (2005)
Bergstra, J.A., Middelburg, C.A.
We present an extension of the polarized process algebra BPPA, an algebraic theory about sequential program behaviors. The extension is called thread algebra and is proposed as a tool for the...
Maurer Computers with Single-Thread Control (2005)
Bergstra, J.A., Middelburg, C.A.
We present the development of a theory of stored threads and their execution. The work builds upon Maurer’s theory of computer instructions and the thread algebra of Bergstra et al. The theory...
Preferential Choice and Coordination Conditions (2005)
Bergstra, J.A., Middelburg, C.A.
We present a process algebra with conditional expressions of which the conditions concern the enabledness of actions in the context in which a process is placed. With those conditions, it becomes...
Process Algebra with Conditionals in the Presence of Epsilon (2005)
Bergstra, J.A., Middelburg, C.A.
In a previous paper, we presented several extensions of ACP with conditional expressions, including one with a retrospection operator on conditions to allow for looking back on conditions under which...
A Bypass of Cohen’s Impossibility Result (2005)
Detecting illegal resource access in the setting of grid computing is similar to the problem of virus detection as put forward by Fred Cohen in 1984. We discuss Cohen’s impossibility result on...
Network algebra in Java (2005)
Network algebra descriptions are translated uniformly to Java yielding a component based simulation model. The model is used to reflect the characteristics of real-world systems.
Process algebra for hybrid systems (2005)
Bergstra, J.A., Middelburg, C.A.
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,...
Strong Splitting Bisimulation Equivalence (2005)
Bergstra, J.A., Middelburg, C.A.
We present ACPc, a process algebra with conditional expressions in which the conditions are taken from a Boolean algebra, and extensions of this process algebra with mechanisms for condition...
Polarized process algebra with reactive composition (2005)
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...
Software ENgineering About "trivial " software patents: the IsNot case (2005)
CWI is a founding member of ERCIM, the European Research Consortium for Informatics and Mathematics. CWI's research has a theme-oriented structure and is grouped into four clusters. Listed below...
A thread algebra with multi-level strategic interleaving (2005)
J. A. Bergstra, C. A. Middelburg
Abstract. In a previous paper, we developed an algebraic theory of threads and multi-threads based on strategic interleaving. This theory includes a number of plausible interleaving strategies on...
Strong splitting bisimulation equivalence (2005)
J. A. Bergstra, C. A. Middelburg
Abstract. We present ACP c, a process algebra with conditional expressions in which the conditions are taken from a Boolean algebra, and extensions of this process algebra with mechanisms for...
A thread algebra with multi-level strategic interleaving (2005)
J. A. Bergstra, C. A. Middelburg
Abstract. In a previous paper, we developed an algebraic theory of threads and multi-threads based on strategic interleaving. This theory includes a number of plausible interleaving strategies on...
A thread algebra with multi-level strategic interleaving (2005)
J. A. Bergstra, C. A. Middelburg
Abstract. In a previous paper, we developed an algebraic theory of threads and multi-threads based on strategic interleaving. This theory includes a number of plausible interleaving strategies on...
A thread algebra with multi-level strategic interleaving (2005)
J. A. Bergstra, C. A. Middelburg
Abstract 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...
Strong splitting bisimulation equivalence (2005)
J. A. Bergstra, C. A. Middelburg
Abstract. We present ACP c, a process algebra with conditional expressions in which the conditions are taken from a Boolean algebra, and extensions of this process algebra with mechanisms for...
Linear Projective Program Syntax (2004)
Based on an extremely simple program notation more advanced program features can be developed in linear projective program syntax such as conditional statements, while loops, recursion, use of an...
Machine function based control code algebras (2004)
Machine functions have been introduced by Earley and Sturgis in [6] in order to provide a mathematical foundation of the use of the T-diagrams proposed by Bratman in [5]. Machine functions describe...
Execution Architectures for Program Algebra (2004)
We investigate the notion of an execution architecture in the setting of the program algebra PGA, and distinguish two sorts of these: analytic architectures, designed for the purpose of explanation...
Continuity controlled Hybrid Automata (2004)
Bergstra, J.A., Middelburg, C.A.
We investigate the connections between the process algebra for hybrid systems of Bergstra and Middelburg and the formalism of hybrid automata of Henzinger et al. We give interpretations of hybrid...
SNABOK, a system an network administration body of knowledge, is coined as an attempt to complement the well-known and quite influential SWEBOK (software engineering body of knowledge) for the less...
Process algebra for Hybrid systems (2004)
Bergstra, J.A., Middelburg, C.A.
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, Chap. 4,...
Continuity Controlled Hybrid Automata (2004)
Bergstra, J.A., Middelburg, C.A.
We investigate the connections between the process algebra for hybrid systems of Bergstra and Middelburg and the formalism of hybrid automata of Henzinger et al. We give interpretations of hybrid...
Linear Projective Program Syntax (2004)
Based on an extremely simple program notation more advanced program features can be developed in linear projective program syntax such as conditional statements, while loops, recursion, use of an...
Model Theory for Process Algebra (2004)
Bergstra, J.A., Middelburg, C.A.
We present a first-order extension of the algebraic theory about processes known as ACP and its main models. Useful predicates on processes, such as deadlock freedom and determinism, can be added to...
Thread Algebra with Multi-Level Strategic Interleaving (2004)
Bergstra, J.A., Middelburg, C.A.
In a previous paper, we developed an algebraic theory of threads and multi-threads based on strategic interleaving. This theory includes a number of plausible interleaving strategies on thread...
Located Actions in Process Algebra with Timing (2004)
Bergstra, J.A., Middelburg, C.A.
We propose a process algebra obtained by adapting the process algebra with continuous relative timing from Baeten and Middelburg [Process Algebra with Timing, Springer, 2002, Chap. 4] to spatially...
Model Theory For Process Algebra (2004)
J. A. Bergstra, C. A. Middelburg
Abstract. We present a first-order extension of the algebraic theory about processes known as ACP and its main models. Useful predicates on processes, such as deadlock freedom and determinism, can be...
Branching time and orthogonal bisimulation equivalence (2003)
We propose a refinement of branching bisimulation equivalence that we call orthogonal bisimulation equivalence. Typically, internal activity (the performance of τ-steps) may be compressed, but not...
Operator programs and operator processes (2003)
We define a notion of program which is not a computer program but an operator program: a detailed description of actions performed and decisions taken by a human operator (computer user) performing a...
Polarized process algebra and program equivalence (2003)
The basic polarized process algebra is completed yielding as a projective limit a cpo which also comprises infinite processes. It is shown that this model serves in a natural way as a semantics for...
Process algebra for hybrid systems (2003)
J. A. Bergstra, C. A. Middelburg
Abstract. 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,...
J. A. Bergstra, C. A. Middelburg
Abstract. We propose a process algebra obtained by adapting the process algebra with continuous relative timing from Baeten and Middelburg [Process Algebra with Timing, Springer, Chap. 4, 2002] to...
Combining programs and state machines (2002)
State machines consume and process actions complementary to programs issuing actions. State machines maintain a state and reply with a boolean response to each action in their interface. As state...
Molecular dynamics is a model for the structure and meaning of object based programming systems. In molecular dynamics the memory state of a system is modeled as a fluid consisting of a collection of...
Molecule-oriented programming in Java (2002)
Molecule-oriented programming is introduced as a programming style carrying some perspective for Java. A sequence of examples is provided. Supporting the development of the molecule-oriented...
Program algebra for sequential code (2002)
The jump instruction is considered essential for an adequate theoretical understanding of imperative sequential programming. Using basic instructions and tests as a basis we outline an algebra of...
Process algebra and conditional composition (2001)
We discern three non-classical truth values, and define a five-valued propositional logic. We combine this logic with process algebra via conditional composition (i.e., if-then-else-). In particular,...
Register-Machine Based Processes (2001)
study extensions of the process algebra axiom system ACP with two recursive operations: the binary Kleene star *, which is defined by x*y = x(x*y)+ y, and the push-down operation $, defined by x$y =...
Syntax and semantics of a high-level intermediate representation for ASF+SDF (2000)
Developing a compiler for ASF+SDF has been a challenging task. The compilation of ASF+SDF is performed using an intermediate language μASF, an abstract syntax representation of ASF+SDF. Although...
Platforms, specifications and decisions (2000)
Program variables in a call-by-value mode are added to the elementary syntax of program algebra. Only very simple data are considered: finite sequences of bits. The meaning of program variables, data...
Program Algebra for Component Code (2000)
The jump instruction is considered essential for an adequate theoretical understanding of imperative sequential programming. Using atomic actions and tests as a basis we outline an algebra of...
Program Algebra and Coprogram Calculus (2000)
On the basis of the program notation PGLD of program algebra, a program notation PGLDg (PGLD with goto's) is proposed with indirect absolute jumps. An indirect absolute jump, also called a goto...
Branching Time and Orthogonal Bisimulation Equivalence (2000)
J. A. Bergstra, A. Ponse, Issn -x, Jan A. Bergstra, Alban Ponse, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Syntax and semantics of a high-level intermediate representation of ASF+SDF (2000)
J. A. Bergstra, J. A. Bergstra
Syntax and semantics of a high-level intermediate representation
Mode Transfer in Process Algebra (2000)
This paper provides a systematic and full treatment of mode transfer operators in process algebra, including complete axiomatizations, operational rules, analysis of expressive power and extensions...
Data Flow Networks in Java (2000)
J.A. Bergstra, I. Bethke, A. Ponse
A survey of examples is produced highlighting the various features and possibilities with pipes and sockets in Java. An implementation of dataow networks is presented and a realization of the...
Reniers. Discrete time process algebra with silent step (2000)
The axiom system ACP of [10] was extended to discrete time in [6]. Here, we proceed to define the silent step in this theory in branching bisimulation semantics [7, 15] rather than weak bisimulation...
Platform projections, compilers, interpreters and portability (1999)
Platform projection semantics extends projection semantics by means of the encapsulation of a processor used for program execution. Platform projection semantics abstracts from platform specific...
Software mechanics for Java multi-threading (1999)
For a subset JavaTck (Java Thread Composition Kernel) of Java an empirical semantics has been developed. Special emphasis is put on the role of synchronization features. The validity of empirical...
Emperical semantics for object-oriented programs (1999)
The focus is on object orientation in a sequential or single-threaded setting and with single inheritance. The second restriction points in the direction of Java1, the rst restriction calls for a...
Programs, interfaces and components (1999)
The jump instruction is considered essential for an adequate theoretical understanding of imperative sequential programming. Using atomic actions and tests as a basis we outline an algebra of...
Empirical semantics for object-oriented programs (1999)
Jan Bergstra, Marijke Loots, J. A. Bergstra, M. E. Loots
2
Software Mechanics for Java Multi-Threading (1999)
For a subset JavaTck (Java Thread Composition Kernel) of Java an empirical semantics has been developed. 1 Special emphasis is put on the role of synchronization features. The validity of empirical...
Deadlock Behaviour in Split and ST Bisimulation Semantics (1998)
Baeten, J.C.M., Bergstra, J.A.
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...
The discrete time TOOLBUS - A software coordination architecture (1998)
The notion of “time” plays an important role when coordinating large, heterogeneous, distributed software systems. We present a generic coordination architecture that supports relative and...
Kleene’s three-valued logic and process algebra (1998)
We propose a combination of Kleene’s three-valued logic and ACP process algebra via the guarded command construct. We present an operational semantics in SOS-style, and a completeness result.
Bochvar-McCarthy logic and process algebra (1998)
We propose a combination of Bochvar's strict three-valued logic, McCarthy's sequential three-valued logic, and process algebra via the conditional guard construct. This combination entails the...
Discrete Time Process Algebra and the Semantics of SDL (1998)
Issn -x, J. A. Bergstra, J. A. Bergstra, C. A. Middelburg, C. A. Middelburg, Y. S. Usenko, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Discrete-time Process Algebra and the Semantics of SDL (1998)
Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, J.A. Bergstra, J. A. Bergstra, C. A. Middelburg, ...
We present an extension of discrete time process algebra with relative timing where recursion, propositional signals and conditions, a counting process creation operator, and the state operator are...
Discrete Time Process Algebra and the Semantics of SDL (1998)
J.A. Bergstra, C.A. Middelburg, Y.S. Usenko
We present an extension of discrete time process algebra with relative timing where recursion, propositional signals and conditions, a counting process creation operator, and the state operator are...
Bounded Stacks, Bags and Queues (1997)
Baeten, J.C.M., Bergstra, J.A.
We prove that a bounded stack can be specified in process algebra with just the operators alternative and sequential composition and iteration. The bounded bag cannot be specified with these...
Process algebra with propositional signals (1997)
Bergstra, J.A., Baeten, J.C.M.
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...
Discrete Time Network Algebra for a Semantic Foundation of SDL (1997)
J.A. Bergstra, C. A. Middelburg, R. Soricut
We propose a process algebra model of asynchronous dataflow networks as a semantic foundation for the specification language SDL. The model, which extends a model of network algebra, is close to the...
Network Algebra for Asynchronous Dataflow (1997)
J.A. Bergstra, C. A. Middelburg, Gh. Stefanescu
Network algebra is proposed as a uniform algebraic framework for the description and analysis of dataflow networks. An equational theory of networks, called BNA (Basic Network Algebra), is presented....
A logic for signal inserted timed frames (1996)
Bergstra, J.A., Fokkink, W.J., Middelburg, K.
We propose a first-order predicate logic TFL of timed frames extended with signals. This logic combines a simple syntax with a high expressivity; it can distinguish frames that are not the same as...
Discrete time process algebra (1996)
Bergstra, J.A., Baeten, J.C.M.
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...
The toolbus coordination architecture (1996)
Building large, heterogeneous, distributed software systems poses serious problems for the software engineer; achieving interoperability of software systems is still a major challenge. We describe an...
A complete transformational toolkit for compilers (1996)
J. A. Bergstra, T. B. Dinesh, J. Heering
Abstract. In an earlier paper, one of the present authors presented a preliminary account of an equational logic called PIM. PIM is intended to function as a "transformational toolkit...
Towards a Complete Transformational Toolkit for Compilers (1996)
J. Field, Issn -x, J.A. Bergstra, J. A. Bergstra, T.B. Dinesh, T. B. Dinesh, ...
Pim is an equational logic designed to function as a "transformational toolkit" for compilers and other programming tools that analyze and manipulate imperative languages. It has been...
J. Field, J. Heering, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, ...
In an earlier paper, one of the present authors presented a preliminary account of an equational logic called PIM. PIM is intended to function as a "transformational toolkit" to be used by...
Complete Transformational Toolkit For Compilers (1996)
J.A. Bergstra, T.B. Dinesh, J. Field, J. Heering
In an earlier paper, one of the present authors presented a preliminary account of an equational logic called PIM. PIM is intended to function as a "transformational toolkit" to be used by...
Transformation of Reduction Systems - a view on proving correctness (1996)
Supervisors Prof. Dr, J. A. Bergstra, Dr. P. H. Rodenburg, Bas Luttik, Bas Luttik, Bas Luttik
Reduction Systems : : : : : : : : : : : : : : : : : : : : : : : : : : : : 3 2.3 Term Rewriting Systems : : : : : : : : : : : : : : : : : : : : : : : : : : : : : : 5 2.3.1 Terms : : : : : : : : : : :...
Algebra of Timed Frames (1996)
J.A. Bergstra, W.J. Fokkink, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Algebra of Timed Frames (1996)
Bergstra Fokkink, J. A. Bergstra, C. A. Middelburg
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Algebra of Timed Frames (1995)
Bergstra, J.A., Fokkink, W.J., Middelburg, C.A.
Timed frames are introduced as objects that can form a basis of a model theory for discrete time process algebra. An algebraic setting for timed frames is proposed and results concerning its...
Process Algebra Semantics of φSDL (1995)
Bergstra, J.A., Middelburg, C.A.
A new semantics of an interesting subset of the specification language SDL is given by a translation to a discrete-time variant of process algebra in the form of ACP extended with data as in μCRL....
The data type variety of stack algebras (1995)
We define and study the class of all stack algebras as the class of all minimal algebras in a variety defined by an infinite recursively enumerable set of equations. Among a number of results, we...
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...
Processes with multiple entries and exits (1995)
Bergstra, J.A., Stefanescu, G.
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...
Discrete time process algebra with abstraction (1995)
Bergstra, J.A., Baeten, J.C.M.
The axiom system ACP of [BEK84a] was extended to cliscrete time in [BAB95]. Here we proceed to define the silent step in this theory in branching bisimulation semantics [GLW91, BAW90] rather than...
Logic of transition systems (1995)
Benthem, Johan Van, Bergstra, J.A.
Labeled transition systems are key structures for modeling computation. In this paper, we show how they lend themselves to ordinary logical analysis (without any special new formalisms), by...
Network Algebra for Synchronous and Asynchronous Dataflow (1995)
J.A. Bergstra, C. A. Middelburg, Gh. Stefanescu
Network algebra is proposed as a uniform algebraic framework for the description and analysis of dataflow networks. An equational theory, called BNA (Basic Network Algebra), is presented. BNA, which...
Process Algebra Semantics of phiSDL (1995)
J.A. Bergstra, C.A. Middelburg
A new semantics of an interesting subset of the specification language SDL is given by a translation to a discrete-time variant of process algebra in the form of ACP extended with data as in ¯CRL....
The Data Type Variety of Stack Algebras (1995)
We define and study the class of all stack algebras as the class of all minimal algberas in a variety defined by an infinite recursively enumerable set of equations. Among a number of results, we...
Some Simple Calculations in Relative Discrete Time Process Algebra (1995)
We do some simple calculations involving bu#ers in discrete time process algebra with relative timing. Note: Dedicated to prof.dr. F.E.J. Kruseman Aretz, on the occasion of his...
Process Algebra with Propositional Signals (1994)
Baeten, J.C.M., Bergstra, J.A.
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...
Network algebra for synchronous and asynchronous dataflow (1994)
Bergstra, J.A., Stefanescu, G.
Network algebra (NA) is proposed as a uniform algebraic framework for the description (and analysis) of dataflow networks. The core of this algebraic setting is provided by an equational theory...
Which data types have ω-complete initial algebra specifications? (1994)
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...
On sequential composition, action prefixes and process prefix (1994)
Bergstra, J.A., Baeten, J.C.M.
We illustrate the difference between sequential composition in process algebra axiomatisations like ACP and action prefixing in process calculi like CCS. We define both early and late input in a...
Process algebra with combinators (1994)
Bergstra, J.A., Bethke, I., Ponse, A.
We introduce typed combinatory process algebra, a system combining process Mgebra with types and combinators. We describe its syntax and semantics, and by way of example, verify within this framework...
Process algebra with partial choice (1994)
Bergstra, J.A., Baeten, J.C.M.
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...
Bisimulation is two-way simulation (1994)
Bergstra, J.A., Stefanescu, G.
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...
Process Algebra with Backtracking (1994)
. An extension of process algebra for modelling processes with backtracking is introduced. This extension is semantically based on processes that transform data because, in our view, backtracking is...
Processes with Multiple Entries and Exits Modulo Isomorphism and Modulo Bisimulation (1994)
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...
The ToolBus - a component interconnection architecture - (1994)
Building large, heterogeneous, distributed software systems poses serious problems for the software engineer; achieving interoperability of software systems is still a major challenge. We describe an...
Bisimulation is Two-Way Simulation (1994)
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...
Process Algebra with Iteration and Nesting (1994)
Bergstra, J. A., Bethke, I., Ponse, A.
We introduce iteration in process algebra by means of (the original, binary version of) Kleene's star operation: x*y is the process that chooses between x and y, and upon termination of x has this...
Decidability of bisimulation equivalence for processes generating context-free languages (1993)
Bergstra, J.A., Baeten, J.C.M., Klop, J.W.
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...
Real space process algebra (1993)
Bergstra, J.A., Baeten, J.C.M.
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...
Non interleaving process algebra (1993)
Baeten, J.C.M., Bergstra, J.A.
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)...
Hidden Sorts, J. A. Bergstra, J. A. Bergstra, J. Heering, J. Heering
Homomorphism preserving algebraic specifications require
Homomorphism Preserving Algebraic Specifications Require Hidden Sorts (1993)
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....
Asynchronous communication in real space process algebra (1992)
Bergstra, J.A., Baeten, J.C.M.
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...
Real-time process algebra (1991)
Bergstra, J.A., Baeten, J.C.M.
We describe an axiom system ACPp 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...
Recursive process definitions with the state operator (1991)
Bergstra, J.A., Baeten, J.C.M.
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...
Design of a specification language by abstract syntax engineering (1991)
Baeten, J.C.M., Bergstra, J.A.
In this paper, we design a specification language in an entirely algebraic style. We describe the language in terms of abstract syntax only. We argue that this is the correct approach in language...
J. A. Bergstra, J. Heering, Thy Nether, J. A. Bergstra, J. Heering
data types have w-complete initial algebra specifications?*
Algebra of states and transitions (1989)
We describe an algebraic specification of an abstract syntax for the construction of sequential transition systems. In these transition systems actions and states have an equally explicit role. Then...
Term rewriting systems with rule priorities (1989)
Bergstra, J.A., Baeten, J.C.M., Klop, J.W., Weijland, W.P.
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...
Process Theory based on Bisimulation Semantics (1989)
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...
A new axiom system BMACP combines the axiom systems BMA (basic module algebra) and ACP (algebra of communicating processes) in such a way that the addition operator (+) which stands for module...
New operators are introduced on top of ACP [BK 84] in order to incorporate stable signals in process algebra. Semantically this involves assigning labels to nodes of process graphs. The labels of...
Readies and failures in the algebra of communicating processes (1988)
Readiness and failure semantics are studied in the setting of Algebra of Communicating Processes (ACP). A model of process graphs modulo readiness equivalence, respectively, failure equivalence, is...
Process algebra semantics for queues (1987)
An unbounded queue over a finite set of data values, is a process Q in Aoo defined by an infinite system of guarded equations. The aim of this paper is to show that no finite system of guarded...
On the consistency of Koomen's fair abstraction rule (1987)
Bergstra, J.A., Baeten, J.C.M., Klop, J.W.
We construct a graph model for ACP,, the algebra of communicating processes w%h silent steps, in which Koomen’s Fair Abstraction Rule (KFAR) holds, and also versions of the Approximation Induction...
Algebraic specifications of computable and semi-computable data structures (1987)
An extensive survey is given of the properties of various specification mechanisms based on initial algebra semantics
Decidability of bisimulation equivalence for processes generating context-free languages (1987)
Bergstra, J.A., Baeten, J.C.M., Klop, J.W.
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 a process can be assigned...
Ready-Trace Semantics for Concrete Process Algebra with the Priority Operator (1987)
Baeten, J. C. M., Bergstra, J. A., Klop, J. W.
We consider a process semantics intermediate between bi-simulation semantics and readiness semantics, called here ready-trace semantics. The advantage of this semantics is that, while retaining the...
Module algebra for relational specifications (1986)
Module algebra is described as a parametrised data type that takes a three sorted parameter, involving signatures, renamings and atomic specifications. An actual parameter describing relational...
Conditional rewrite rules : confluence and termination (1986)
Algebraic specifications of abstract data types can often be viewed as systems of rewrite rules. Here we consider rewrite rules with conditions, such as they arise, e.g., from algebraic...
Verification of an alternating bit protocol by means of process algebra (1986)
We verify a simple verslon of the alternating bit protocol in the system ACP- (Algebra of Communicating Processes with silent actions) augmented with Koomenls falr abstraction rule.
Module algebra for relational specifications (1986)
Module algebra is described as a parametrised data type that takes a three sorted parameter, involving signatures, renamings and atomic specifications. An actual parameter describing relational...
A process creation mechanism in process algebra (1985)
We introduce an encapsulation operator Eφ that provides process algebra with a process creation mechanism. Several simple examples are considered. It is shown that Eφ does not extend the defining...
Algebra of communicating processes with abstraction (1985)
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...
Put and get, primitives for synchronous unreliable message passing (1985)
Two message passing mechanisms are described. These mechanisms areboth synchronous and unreliable. Within concrete process algebra with 6 operator for priorities these mechanisms, called put and get...
Hoare's logic for programming languages with two datatypes (1984)
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...
Linear time and branching time semantics for recursion with merge (1984)
Bergstra, J.A., Bakker, J.W. De, Meyer, J-J.Ch., Klop, J.W.
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...
Proving program inclusion using Hoare's logic (1984)
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...
Top-down design and the algebra of communicating processes (1984)
We develop an algebraic theory for the top-down design of communicating systems in which levels of abstraction are represented by algebras, and their stepwise refinements are represented by...
Process algebra for synchronous communication (1984)
Within the context of an algebraic theory of processes, an equational specification of process cooperation is provided. Four cases are considered: free merge or interleaving, merging with...
Standard model semantics for DSL, a data type specification language (1983)
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 (∑,...
A proof rule for restoring logic circuits (1983)
An axiomatic semantics is given for restoring logic circuits, both statically and dynamically. As an example the Muller C-element is discussed in detail. It is shown that a consistent circuit reacts...
Preprint: A proof rule for restoring logic circuits (1983)
An axiomatic semantics is given for restoring logic circuits, both statically and dynamically. As an example the Muller C-element is discussed in detail. It is shown that a consistent circuit reacts...
Floyd's principle, correctness theories and program equivalence (1982)
Bergstra, J.A., Tiuryn, J., Tucker, J.V.
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...
Expressiveness and the completeness of Hoare's logic (1982)
Three theorems are proven which reconsider the completeness of Hoare's logic for the partial correctness of while-programs equipped with a first-order assertion language. The results are about the...
We conceive a parametrized data type as a partial functor φ: ALG (∑) --> ALG (Δ), where Δ is a signature extending ∑ and ALG (∑) is the class of minimal ∑-algebras which serve as...
A convergence theorem in process algebra (1982)
We study a convergence phenomenon in the projective limit model A°° for PA, an axiom system in the framework of process algebra for processes built from atomic actions by means of alternative....
On the power of algebraic specifications (1981)
Bergstra, J.A., Broy, M., Tucker, J.V., Wirsing, M.
We study the expressive power of different algebraic specification methods. In contrast to (nonhierarchical) initial and terminal algebra specifications which correspond to semicomputable and...
Regular extensions of iterative algebras and metric interpretations (1981)
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...
Implicit definability of algebraic structures by means of program properties (1981)
The following problem is investigated in the paper: what structures can be uniquely defined, by algorithmic properties? The algorithmic propertifa are represented in this paper as open formulae of...
With the term Hoare-Zike lugic we have in mind some proof system designed for the formal manipulation of assertions about the partial correctnesls of program texts witR respect to a tied...
Computability and continuity in finite types / (1976)
Thesis - Rijksuniversiteit te Utrecht, 1976.
Network Algebra with Demonic Relation Operators
J.A. Bergstra, Gheorghe Stefanescu
Relations with demonic operators are used in studies related to predicate transformer semantics of nondeterministic programs, to model the connection wires in synchronous dataflow networks, or in...
We consider process graphs over a set of pins, i.e. with multiple entries and exits. On process graphs modulo bisimulation, we can define all standard process algebra operators plus the feedback...
Network Algebra for Synchronous and Asynchronous Dataflow
Network algebra (NA) is proposed as a uniform algebraic framework for the description (and analysis) of dataflow networks. The core of this algebraic setting is provided by an equational theory...
Timed tuplix calculus and the Wesseling and van den Bergh equation
J. A. Bergstra, C. A. Middelburg
We formalize a cumulative interest compliant conservation requirement for pure financial products proposed by Wesseling and van den Bergh to make financial issues relating to these products amenable...