arXiv subjects

C. A. Middelburg

Publications and source records attributed to C. A. Middelburg.

At least 19 recordsLinked to original sources

arXiv2026

Probabilistic imperative process algebra

In a previous paper, a process algebra based on ACP (Algebra of Communicating Processes) was proposed in which processes involving data can be handled by means of features originating from imperative programming. In this paper, an extension of that process algebra with probabilistic choice operators is presented that rests on the principle that probabilistic choices are always resolved before choices involved in alternative composition and parallel composition are resolved. This extension is devised, among other things, to be used for modeling and analyzing algorithms that are important in the area of distributed computing. Many canonical problems in that area call for a probabilistic algorithm. In this paper, a probabilistic algorithm for the leader election problem is modeled using the presented process algebra.

cs.LO↗

arXiv2026

On an ordinary expansion of first-order Belnap-Dunn logic

This paper concerns an expansion of first-order Belnap-Dunn logic whose connectives and quantifiers all have a counterpart in classical logic. The language and logical consequence relation of this paradefinite logic are defined, a sequent calculus proof system for this logic is presented, and the soundness and completeness of this proof system is established. It is shown that the defined logic distinguishes itself from the many other paradefinite logics that are usually considered equally classical by the classical laws of logical equivalence that hold for it. It is further argued that the defined logic is the most natural paradefinite logic relative to the version of classical logic with the same language. Moreover, a simple embedding of the defined logic in that version of classical logic is presented and the potential of the logic for dealing with inconsistencies and incompletenesses in inductive machine learning is discussed.

cs.LO↗

arXiv2026

The most natural paradefinite logic relative to classical logic

A paradefinite logic is a logic that can serve as the underlying logic for theories that are inconsistent or incomplete. A well-known paradefinite logic is Belnap-Dunn logic. Various expansions of Belnap-Dunn logic have been studied in the literature. In this note, it is argued that the most natural paradefinite logic relative to classical logic is the expansion of Belnap-Dunn logic with a falsity connective and an implication connective for which the standard deduction theorem holds.

math.LO↗

arXiv2025

Formalizing the notions of non-interactive and interactive algorithms

An earlier paper gives an account of a quest for a satisfactory formalization of the classical informal notion of an algorithm. That notion only covers algorithms that are deterministic and non-interactive. In this paper, an attempt is made to generalize the results of that quest first to a notion of an algorithm that covers both deterministic and non-deterministic algorithms that are non-interactive and then further to a notion of an algorithm that covers both deterministic and non-deterministic algorithms that are interactive. The notions of an non-interactive proto-algorithm and an interactive proto-algorithm are introduced. Non-interactive algorithms and interactive algorithms are expected to be equivalence classes of non-interactive proto-algorithms and interactive proto-algorithms, respectively, under an appropriate equivalence relation. On both non-interactive proto-algorithms and interactive proto-algorithms, three equivalence relations are defined. Two of them are deemed to be bounds for an appropriate equivalence relation and the third is likely an appropriate one.

cs.CC↗

arXiv2025

On the formalization of the notion of a concurrent algorithm

Previous papers give accounts of quests for satisfactory formalizations of the classical informal notion of an algorithm and the contemporary informal notion of an interactive algoritm. In this paper, an attempt is made to generalize the results of the former quest to the contemporary informal notion of a concurrent algorithm. The notion of a concurrent proto-algorithm is introduced. The thought is that concurrent algorithms are equivalence classes of concurrent proto-algorithms under an appropriate equivalence relation. Three equivalence relations are defined. Two of them are deemed to be bounds for an appropriate equivalence relation and the third is likely an appropriate one. The connection between concurrency and non-determinism in the presented setting is also addressed.

cs.CC↗

arXiv2025

Complementing an imperative process algebra with a rely/guarantee logic

This paper concerns the relation between imperative process algebra and rely/guarantee logic. An imperative process algebra is complemented by a rely/guarantee logic that can be used to reason about how data change in the course of a process. The imperative process algebra used is the extension of ACP (Algebra of Communicating Processes) that is used earlier in a paper about the relation between imperative process algebra and Hoare logic. A complementing rely/guarantee logic that concerns judgments of partial correctness is treated in detail. The adaptation of this logic to weak and strong total correctness is also addressed. A simple example is given that suggests that a rely/guarantee logic is more suitable as a complementing logic than a Hoare logic if interfering parallel processes are involved.

cs.LO↗

arXiv2025

A classical-logic view on a paraconsistent logic

This paper is concerned with the paraconsistent first-order logic LPQ$^{\supset,\mathsf{F}}$, Priest's LPQ enriched with an implication connective and a falsity constant. A sequent-style natural deduction proof system for this logic is presented and, for this proof system, both a model-theoretic justification and a logical justification by means of an embedding into first-order classical logic is given. The given embedding provides in addition a classical-logic explanation of this paraconsistent logic. As a further matter, its use in decidability issues concerning this paraconsistent logic is discussed. The major properties of LPQ$^{\supset,\mathsf{F}}$ concerning its logical consequence relation and its logical equivalence relation are also treated. The paper emphasizes how closely LPQ$^{\supset,\mathsf{F}}$ is related to classical logic.

cs.LO↗

arXiv2025

The interdefinability of expansions of Belnap-Dunn logic

Belnap-Dunn logic, also knows as the logic of First-Degree Entailment, is a logic that can serve as the underlying logic of theories that are inconsistent or incomplete. For various reasons, different expansions of Belnap-Dunn logic with non-classical connectives have been studied. This paper investigates the question whether those expansions are interdefinable with an expansion whose connectives include only classical connectives. Surprisingly, this relevant question is not addressed anywhere in the published studies. The notion of interdefinability of logics used is based on a general notion of definability of a connective in a logic that seems to have been forgotten. Attention is also paid to the extent to which the expansion whose connectives include only classical connectives is related to the version of classical logic with the same connectives.

cs.LO↗

arXiv2025

Space-time process algebra with asynchronous communication

We introduce a process algebra that concerns the timed behaviour of distributed systems with a known spatial distribution. This process algebra provides a communication mechanism that deals with the fact that a datum sent at one point in space can only be received at another point in space at the point in time that the datum reaches that point in space. The variable-binding integration operator used in related process algebras to model such a communication mechanism is absent from this process algebra. This is considered an advantage because the variable-binding operator does not really fit in with an algebraic approach and a process algebra with this operator is not firmly founded in established metatheory.

cs.LO↗

arXiv2024

On the formalization of the notion of an algorithm

The starting point of this paper is a collection of properties of an algorithm that have been distilled from the informal descriptions of what an algorithm is that are given in standard works from the mathematical and computer science literature. Based on that, the notion of a proto-algorithm is introduced. The thought is that algorithms are equivalence classes of proto-algorithms under some equivalence relation. Three equivalence relations are defined. Two of them give bounds between which an appropriate equivalence relation must lie. The third lies in between these two and is likely an appropriate equivalence relation. A sound method is presented to prove, using an imperative process algebra based on ACP, that this equivalence relation holds between two proto-algorithms.

cs.CC↗

arXiv2023

Dormancy-aware timed branching bisimilarity, with an application to communication protocol analysis

A variant of the standard notion of branching bisimilarity for processes with discrete relative timing is proposed which is coarser than the standard notion. Using a version of ACP (Algebra of Communicating Processes) with abstraction for processes with discrete relative timing, it is shown that the proposed variant allows of both the functional correctness and the performance properties of the PAR (Positive Acknowledgement with Retransmission) protocol to be analyzed. In the version of ACP concerned, the difference between the standard notion of branching bisimilarity and its proposed variant is characterized by a single axiom schema.

cs.LO↗

arXiv2023

Imperative process algebra and models of computation

Studies of issues related to computability and computational complexity involve the use of a model of computation. Pivotal to such a model are the computational processes considered. Processes of this kind can be described using an imperative process algebra based on ACP (Algebra of Communicating Processes). In this paper, it is investigated whether the imperative process algebra concerned can play a role in the field of models of computation.It is demonstrated that the process algebra is suitable to describe in a mathematically precise way models of computation corresponding to existing models based on sequential, asynchronous parallel, and synchronous parallel random access machines as well as time and work complexity measures for those models. A probabilistic variant of the model based on sequential random access machines and complexity measures for it are also described.

cs.LO↗

arXiv2023

Belnap-Dunn logic and query answering in inconsistent databases with null values

This paper concerns an expansion of first-order Belnap-Dunn logic, named $\mathrm{BD}^{\supset,\mathsf{F}}$, and an application of this logic in the area of relational database theory. The notion of a relational database, the notion of a query applicable to a relational database, and several notions of an answer to a query with respect to a relational database are considered from the perspective of this logic, taking into account that a database may be an inconsistent database or a database with null values. The chosen perspective enables among other things the definition of a notion of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. For each of the notions of an answer considered, being an answer to a query with respect to a database of the kind considered is decidable.

cs.DB↗

arXiv2023

Paraconsistent logic and query answering in inconsistent databases

This paper concerns the paraconsistent logic LPQ$^{\supset,\mathsf{F}}$ and an application of it in the area of relational database theory. The notions of a relational database, a query applicable to a relational database, and a consistent answer to a query with respect to a possibly inconsistent relational database are considered from the perspective of this logic. This perspective enables among other things the definition of a consistent answer to a query with respect to a possibly inconsistent database without resort to database repairs. In a previous paper, LPQ$^{\supset,\mathsf{F}}$ is presented with a sequent-style natural deduction proof system. In this paper, a sequent calculus proof system is presented because it is common to use a sequent calculus proof system as the basis of proof search procedures and such procedures may form the core of algorithms for computing consistent answers to queries.

cs.DB↗

arXiv2022

Program algebra for random access machine programs

This paper presents an algebraic theory of instruction sequences with instructions for a random access machine (RAM) as basic instructions, the behaviours produced by the instruction sequences concerned under execution, and the interaction between such behaviours and RAM memories. This theory provides a setting for the development of theory in areas such as computational complexity and analysis of algorithms that distinguishes itself by offering the possibility of equational reasoning to establish whether an instruction sequence computes a given function and being more general than the setting provided by any known version of the RAM model of computation. In this setting, a semi-realistic version of the RAM model of computation and a bit-oriented time complexity measure for this version are introduced. Under the time measure concerned, semi-realistic RAMs can be simulated by multi-tape Turing machines with quadratic time overhead.

cs.PL↗

arXiv2022

Imperative process algebra with abstraction

This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction of this kind opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established.

cs.LO↗

arXiv2020

On the strongest three-valued paraconsistent logic contained in classical logic and its dual

LP$^{\supset,\mathsf{F}}$ is a three-valued paraconsistent propositional logic which is essentially the same as J3. It has most properties that have been proposed as desirable properties of a reasonable paraconsistent propositional logic. However, it follows easily from already published results that there are exactly 8192 different three-valued paraconsistent propositional logics that have the properties concerned. In this paper, properties concerning the logical equivalence relation of a logic are used to distinguish LP$^{\supset,\mathsf{F}}$ from the others. As one of the bonuses of focussing on the logical equivalence relation, it is found that only 32 of the 8192 logics have a logical equivalence relation that satisfies the identity, annihilation, idempotent, and commutative laws for conjunction and disjunction. For most properties of LP$^{\supset,\mathsf{F}}$ that have been proposed as desirable properties of a reasonable paraconsistent propositional logic, its paracomplete analogue has a comparable property. In this paper, properties concerning the logical equivalence relation of a logic are also used to distinguish the paracomplete analogue of LP$^{\supset,\mathsf{F}}$ from the other three-valued paracomplete propositional logics with those comparable properties.

cs.LO↗

arXiv2020

Using Hoare logic in a process algebra setting

This paper concerns the relation between process algebra and Hoare logic. We investigate the question whether and how a Hoare logic can be used for reasoning about how data change in the course of a process when reasoning equationally about that process. We introduce an extension of ACP (Algebra of Communicating Processes) with features that are relevant to processes in which data are involved, present a Hoare logic for the processes considered in this process algebra, and discuss the use of this Hoare logic as a complement to pure equational reasoning with the equational axioms of the process algebra.

cs.LO↗