计算机科学中的逻辑

Using Isabelle/HOL, we verify a union-find data structure with an explain operation due to Nieuwenhuis and Oliveras. We devise a simpler, more naive version of the explain operation whose soundness and completeness is easy to verify. Then,…

This dialog paper offers a preview and provides a foretaste of an upcoming work on the axiomatization of basic interactive algorithms. The modern notion of algorithm was elucidated in the 1930s--1950s. It was axiomatized a quarter of a…

We introduce the family of multi-modal logics of bounded density and with a tableau-like approach using finite \emph{windows} which were introduced in \cite{BalGasq25} and that we generalize to recursive windows. We prove that their…

In \cite{Lyon24} the question of the decidability of quasi-dense modal logics is answered, and an upper bound in $\EXPSPACE$ is given. Unfortunately, authors' intricate proof seems to contain a major flaw that cannot be fixed, leaving the…

The program of internal type theory seeks to develop the categorical model theory of dependent type theory using the language of dependent type theory itself. In the present work we study internal homotopical type theory by relaxing the…

We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-order state. To support modular reasoning about concurrent…

Model checking is a technique to automatically assess whether a model of the behaviour of a system meets its requirements. Evidence explaining why the behaviour does (not) meet its requirements is essential for the user to understand the…

This paper establishes relative expressiveness results for several modal mu-calculi interpreted over timed automata. These mu-calculi combine modalities for expressing passage of (real) time with a general framework for defining formulas…

Peterson's mutual exclusion algorithm for two processes has been generalized to $N$ processes in various ways. As far as we know, no such generalization is starvation free without making any fairness assumptions. In this paper, we study the…

Distributed software is very tricky to implement correctly as some errors only occur in peculiar situations. For such errors testing is not effective. Mathematically proving correctness is hard and time consuming, and therefore, it is…

Branching bisimilarity is a behavioural equivalence relation on labelled transition systems that takes internal actions into account. It has the traditional advantage that algorithms for branching bisimilarity are more efficient than all…

We propose a benchmark suite for parity games that includes all benchmarks that have been used in the literature, and make it available online. We give an overview of the parity games, including a description of how they have been…

We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order…

We study the process theoretic notion of stuttering equivalence in the setting of parity games. We demonstrate that stuttering equivalent vertices have the same winner in the parity game. This means that solving a parity game can be…

We analyse the problem of solving Boolean equation systems through the use of structure graphs. The latter are obtained through an elegant set of Plotkin-style deduction rules. Our main contribution is that we show that equation systems…

We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal,…

This paper introduces the notion of control closure certificates to synthesize controllers for discrete-time control systems against $\omega$-regular specifications. Typical functional approaches to synthesize controllers against…

AGI (Strong AI) aims to create intelligent robots that are quasi indistinguishable from the human mind. Like a child, the AGI robot would have to learn through input and experiences, constantly progressing and advancing its abilities over…

The informal question of when two theorem proofs are "essentially the same" goes back to David Hilbert, who considered adding it (or something largely equivalent) to his famous list of open problems, but eventually decided to leave it out.…

We study automatic synthesis of systems that interact with their environment and maintain privacy against an observer to the interaction. The system and the environment interact via sets $I$ and $O$ of input and output signals. The input to…