计算机科学中的逻辑

This paper studies the expected value of multiplicative rewards, where rewards obtained in each step are multiplied (instead of the usual addition), in Markov chains (MCs) and Markov decision processes (MDPs). One of the key differences to…

While there is a long tradition of reasoning about (non)termination in program analysis, specialized logics are typically needed to give different termination criteria. This includes partial correctness, where termination is not guaranteed,…

In this note we provide an algorithm for translating relational structures into "proper" relational structures, i.e., those such that there is no pair of worlds w and u such that w is accessible from u for every agent. In particular, our…

We propose a probabilistic hyperlogic called HyperSt$^2$ that can express hyperproperties of strategies in turn-based stochastic games. To the best of our knowledge, HyperSt$^2$ is the first hyperlogic for stochastic games. HyperSt$^2$ can…

In recent years, various techniques have been explored for the verification of quantum circuits, including the use of barrier certificates, mathematical tools capable of demonstrating the correctness of such systems. These certificates…

Knowledge refactoring compresses a logic program by introducing new rules. Current approaches struggle to scale to large programs. To overcome this limitation, we introduce a constrained optimisation refactoring approach. Our first key idea…

Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection…

Matching logic (ML) was developed by Grigore Ro\c{s}u and collaborators as a logic for defining the formal semantics of programming languages and for specifying and reasoning about the behavior of programs. These lecture notes present basic…

Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and artificial intelligence. A crucial property of BNs is the…

We present a logical framework that enables us to define a formal theory of computational trust in which this notion is analysed in terms of epistemic attitudes towards the possible objects of trust and in relation to existing evidence in…

Many abstract interpretation frameworks and analyses for Prolog have been proposed, which seek to extract information useful for program optimization. Although motivated by practical considerations, notably making Prolog competitive with…

We propose a modular method for proving termination of general logic programs (i.e., logic programs with negation). It is based on the notion of acceptable programs, but it allows us to prove termination in a truly modular way. We consider…

We introduce a Hennessy-Milner logic with recursion for Fresh Labelled Transition Systems (FLTSs). These are nominal labelled transition systems which keep track of the history, i.e. of data values seen so far, and can capture fresh data…

Autonomous systems are often used in changeable and unknown environments, where traditional verification may not be suitable. Runtime Verification (RV) checks events performed by a system against a formal specification of its intended…

In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proof of which…

We present a labelled and non-wellfounded calculus for the bimodal provability logic CS. The system is obtained by modelling the Kripke-like semantics of this logic. As in arXiv:2309.00532, we enforce the second-order property of converse…

We show how several graph problems (e.g., vertex-cover, independent-set, $k$-coloring) can be encoded into CNF using only $O(|V|^2 / \lg |V|)$ many clauses, as opposed to the $\Omega(|V|^2)$ constraints used by standard encodings. This…

The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure termination (AST), while also providing quantitative answers…

This paper presents a novel simplification calculus for propositional logic derived from Peirce's existential graphs' rules of inference and implication graphs. Our rules can be applied to propositional logic formulae in nested form, are…

We present an automata-based algorithm to synthesize omega-regular causes for omega-regular effects on executions of a reactive system, such as counterexamples uncovered by a model checker. Our theory is a generalization of temporal…