计算机科学中的逻辑
These lecture notes provide an introduction to the verification of neural networks from a theoretical perspective. We discuss feed-forward neural networks, recurrent neural networks, attention mechanisms, and transformers, together with…
We study positional properties in the context of game-based reactive synthesis. Our motivation stems from having a usable specification logic, for which tractable synthesis is guaranteed. We demonstrate that every $\omega$-regular…
Aiming to harmonise finite and infinite model reasoning, we initiate the study of partially finite models, where the reasoning task comes with a formula that specifies a part of the model that must be finite. We focus on the problem of…
BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side,…
We introduce a new family of temporal logics intended for specifications in motion planning (MP). It builds upon the signal temporal logic (STL), which is a linear-time logic over real-valued signals that possess quantitative semantics and…
Real numbers in constructive mathematics have always seemed to require compromises of one form or another. Classical proofs of Cauchy completeness require countable choice, Bishop's setoid construction introduces persistent bookkeeping…
The Conway-99 problem questions the existence of a strongly regular graph with 99 vertices and specific parameters. A \textit{strongly} regular graph is a regular graph that exhibits two additional properties: vertices must share a fixed…
We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas…
Systems deployed for long periods of time in dynamic environments may experience performance degradation that affects timing guarantees, even when their functional behaviour remains unchanged. In the design and verification of critical…
In 2008, Bodirsky and Grohe showed that for every $\Pi_n^{\mathrm{P}}$-level of the Polynomial Hierarchy (PH) there are $\omega$-categorical Constraint Satisfaction Problems (CSPs) complete for this level. We show that, in fact, there are…
Formal verification using interactive theorem provers ensures high-quality software. However, writing proof scripts for interactive theorem provers is labor-intensive and requires deep expertise. Recent studies have leveraged deep learning…
The Hanoi Omega-Automata (HOA) format has established itself as the definitive standard for encoding $\omega$-regular automata in modern synthesis tools. While HOA is widely adopted due to its succinct symbolic representation, using Boolean…
We present ZFLean, a Lean 4 library for doing core mathematics inside a model of ZFC with the ergonomics expected of typed Mathlib developments. Building on Mathlib's ZFC model, we contribute a relational calculus for sets with rewriting…
Reliable verification techniques for quantum communication protocols are of paramount importance, given their high implementation cost and critical contexts of application. Extensions of process calculi have been proposed, together with…
We study a variant of the modal $\mu$-calculus based on the constructive modal logic $\mathsf{CK}$. We define game semantics for the constructive $\mu$-calculus and prove its equivalence to the birelational Kripke semantics. We then use the…
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning…
We introduce a logical language for reasoning about quantized aggregate-combine graph neural networks with global readout (ACR-GNNs). We provide a logical characterization and use it to prove that verification tasks for quantized GNNs with…
The radius-$r$ splitter game is played on a graph $G$ between two players: Splitter and Connector. In each round, Connector selects a vertex $v$, and the current game arena is restricted to the radius-$r$ neighborhood of $v$. Then Splitter…
We study the expressive power of first-order logic with counting quantifiers, especially the $k$-variable and quantifier-rank-$q$ fragment, using homomorphism indistinguishability. Recently, Dawar, Jakl, and Reggio~(2021) proved that two…
Converting high-level tasks described by natural language into formal specifications like Linear Temporal Logic (LTL) is a key step towards providing formal safety guarantees over cyber-physical systems (CPS). While the compliance of the…