计算机科学中的逻辑

The higher-dimensional version of Kannan and Lipton's Orbit Problem asks whether it is decidable if a target subspace can be reached from a starting point under repeated application of a linear transformation. Similarly, the continuous…

Despite significant efforts towards extending the AGM paradigm of belief change beyond finitary logics, the computational aspects of AGM have remained almost untouched. We investigate the computability of AGM contraction on non-finitary…

We study the problem of monitoring at runtime whether a system fulfills a specification defined by a hyperproperty, such as linearizability or variants of non-interference. For this purpose, we introduce specifications with both passive and…

Separation logic was conceived in order to make the verification of pointer programs scalable to large systems and it has proven extremely effective. The key idea is that programs typically access only small parts of memory, allowing for…

Causal reasoning is essential for understanding decision-making about the behaviour of complex `ecosystems' of systems that underpin modern society, with security -- including issues around correctness, safety, resilience, etc. -- typically…

Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from…

Parametric Markov chains (pMCs) are Markov chains (MCs) with symbolic probabilities. A pMC encodes a family of MCs, where each member is obtained by replacing parameters with constants. The parameters allow encoding dependencies between…

Safety-critical infrastructures must operate in a safe and reliable way. Fault tree analysis is a widespread method used for risk assessment of these systems: fault trees (FTs) are required by, e.g., the Federal Aviation Administration and…

Standpoint extensions of knowledge representation formalisms have been recently introduced as a means to incorporate multi-perspective modelling and reasoning through modal operators that attribute pieces of knowledge to specific entities…

We propose a method to synthesize a parameterized infinite-state systems that can be instantiated for different parameter values. The specification is given in a parameterized temporal logic that allows for data variables as well as…

We establish a correspondence between (fragments of) $\mathcal{TEL}^\bigcirc$, a temporal extension of the $\mathcal{EL}$ description logic with the LTL operator $\bigcirc^k$, and some specific kinds of formal grammars, in particular,…

Loop invariants are essential for proving the correctness of programs with loops. Developing loop invariants is challenging, and fully automatic synthesis cannot be guaranteed for arbitrary programs. Some approaches have been proposed to…

The Ordinal Folding Index (OFI) is a new, fully computable yard-stick that measures how many rounds of self-reference a statement, protocol or position must unfold before its truth or outcome stabilises. By turning this abstract 'fold-back'…

Formal verification provides assurances that a probabilistic system satisfies its specification--conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We…

We illustrate the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2.

The Value Problem for weighted timed games (wtgs) consists in determining, given a two-player weighted timed game with a reachability objective and a rational threshold, whether or not the value of the game exceeds the threshold. When…

The game of Cops and Robbers is an important model for studying computational queries in pursuit-evasion environments, among others. As recent logical explorations have shown, its structure exhibits appealing analogies with modal logic. In…

This report proposes a formal specification for organising all buildings, streets and administrative areas in the world into a hierarchical space-partitioning tree using data from OpenStreetMap. This hierarchical structure is encoded into a…

Safe Reinforcement Learning focuses on developing optimal policies while ensuring safety. A popular method to address such task is shielding, in which a correct-by-construction safety component is synthesized from logical specifications.…

Combinatorial games played between two players, called Spoiler and Duplicator, have often been used to capture syntactic properties of formal logical languages. For instance, the widely used Ehrenfeucht-Fra\"iss\'e (EF) game captures the…