Author name cluster

Jan A. Bergstra

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

TCS Journal 2025 Journal Article

For rational numbers with Suppes-Ono division, equational validity is one-one equivalent with Diophantine unsolvability

Jan A. Bergstra
John V. Tucker

Adding division to rings and fields leads to the question of how to deal with division by 0. From a plurality of options, we discuss in detail what we call Suppes-Ono division in which division by 0 produces 0. We explain the backstory of this semantic option and its associated notion of equality, and prove a result regarding the logical complexity of deciding equations over the rational numbers equipped with Suppes-Ono division. We prove that deciding the validity of the equations is computationally equivalent to the Diophantine Problem for the rational numbers, which is a longstanding open problem.

Details DOI

TCS Journal 2011 Journal Article

A calculus for four-valued sequential logic

Jan A. Bergstra
Jaco van de Pol

We present a complete axiomatisation for four-valued sequential logic. It consists of nine axioms, from which all valid laws can be derived by equational reasoning. These nine axioms are independent of each other.

Details DOI

TCS Journal 2003 Journal Article

Branching time and orthogonal bisimulation equivalence

Jan A. Bergstra
Alban Ponse
Mark B. van der Zwaag

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 completely discarded. Hence, a process with τ-steps cannot be equivalent to one without τ-steps. Also, we present a modal characterization of orthogonal bisimulation equivalence. This equivalence is a congruence for ACP extended with abstraction and priority operators. We provide a complete axiomatization, and describe some expressiveness results. Finally, we present the verification of a PAR protocol that is specified with use of priorities.

Details DOI

TCS Journal 2001 Journal Article

Non-regular iterators in process algebra

Jan A. Bergstra
Alban Ponse

We consider three forms of non-regular iteration in process algebra: the push-down operation $, defined by x$y=x((x$y)(x$y))+y, the nesting operation ♯, defined by x ♯ y=x((x ♯ y)x)+y, and the back and forth operation ⇆, defined by x ⇆ y=x((x ⇆ y)y)+y. In the process algebraic framework ACP with abstraction and one of $, ♯ or ⇆ we provide definitions of the following standard processes: stack, context-free process, bag, and queue. These definitions apply to all standard behavioural equivalences (we only use xτ=x, where τ is the silent step). Moreover, these results yield the expressive power to express computable processes modulo rooted branching bisimulation equivalence, and hence support the equational founding of process algebra: standard processes can be represented as terms.

Details DOI

CSL Conference 1994 Conference Paper

Process Algebra with Combinators

Jan A. Bergstra
Inge Bethke
Alban Ponse

Abstract We introduce typed combinatory process algebra, a system combining process algebra with types and combinators. We describe its syntax and semantics, and by way of example, verify within this frame-work the Simple Alternating Bit Protocol.

Details

MFCS Conference 1981 Conference Paper

On the Power of Algebraic Specifications

Jan A. Bergstra
Manfred Broy
John V. Tucker
Martin Wirsing

Abstract We study the expressive power of different algebraic specification methods. In contrast to (nonhierarchical) initial and terminal algebra specifications which correspond to semicomputable and cosemicomputable algebras, hierarchical specifications — as e. g. in the specification language CLEAR — allow to specify hyperarithmetical algebras and are characterized by them. For partial abstract types we prove that every computable partial algebra has an equational hidden enrichment specification and discuss the power of hierarchical partial algebras. Finally we give an example of the specification of a simple nondeterministic programming language.

Details

TCS Journal 1979 Journal Article

Recursive assertions are not enough - or are they?

Krzysztof R. Apt
Jan A. Bergstra
Lambert G.L.T. Meertens

Call a set of assertions A complete (with respect to a class of programs S ) if for any p, q∈A and S∈S, wherever {p}S{q} holds, then all intermediate assertions can be chosen from A. This paper is devoted to the study of the problem which sets of assertions are complete in the above sense. We prove that any set of recursive assertions containing true and false is not complete. We prove the completeness for while programs of some more powerful assertions, e. g. the set of recursively enumerable assertions. Finally, we show that by allowing the use of an ‘auxilliary’ coordinate, the set of recursive assertions is complete for while programs.

Details DOI

MFCS Conference 1978 Conference Paper

Decision Problems Concerning Parallel Programming

Jan A. Bergstra

Abstract A notion of a correct (= deadlock free) scheduling of several recursive processes using common resources is introduced. The existence of correct schedulings is schown to be undecidable from recursive indices of the relevant processes. Further-more we isolate several cases where the more existence of a correct scheduling does not imply the existence of a computable (recursive) correct scheduling.

Details