计算机科学中的逻辑

We present a tool called Hoax for the execution of {\omega}-automata expressed in the popular HOA format. The tool leverages the notion of trap sets to enable runtime monitoring of any (non-parity) acceptance condition supported by the…

Recently, interest has increased in applying reactive synthesis to richer-than-Boolean domains. A major (undecidable) challenge in this area is to establish when certain repeating behaviour terminates in a desired state when the number of…

Intuitionistic grammar logics fuse constructive and multi-modal reasoning while permitting the use of converse modalities, serving as a generalization of standard intuitionistic modal logics. In this paper, we provide definitions of these…

We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output…

In the spirit of the Curry-Howard correspondence between proofs and programs, we define and study a syntax and semantics for classical logic equipped with a computationally involutive negation, using a polarised effect calculus, the linear…

This article proves the completeness of an axiomatization for initial value problems (IVPs) with compact initial conditions and compact time horizons for bounded open safety, open liveness and existence properties. Completeness…

We present SBTrust, a logical framework designed to formalize decision trust. Our logic integrates a doxastic modality with a novel non-monotonic conditional operator that establishes a positive support relation between statements, and is…

Lumsdaine (2010) and van den Berg-Garner (2011) proved that types in Martin-L\"of type theory carry the structure of weak {\omega}-groupoids. Their proofs, while foundational, rely on abstract properties of the identity type without…

Hyperproperties allow one to specify properties of systems that inherently involve not single executions of the system, but several of them at once: observational determinism and non-inference are two examples of such properties used to…

The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence -- fixing the truth values of a set of ground…

Threshold automata are a formalism for modeling and analyzing fault-tolerant distributed algorithms, recently introduced by Konnov, Veith, and Widder, describing protocols executed by a fixed but arbitrary number of processes. We conduct…

This paper proposes a novel hybrid neuro-symbolic framework for the optimal and scalable deployment of component-based applications in the Cloud. The challenge of efficiently mapping application components to virtual machines (VMs) across…

The stabiliser fragment of quantum theory is a foundational building block for quantum error correction and the fault-tolerant compilation of quantum programs. In this article, we develop a sound, universal and complete denotational…

This technical report presents a comprehensive formal verification approach for probabilistic agent systems modeling ballistic rocket flight trajectories using Probabilistic Alternating-Time Temporal Logic (PATL). We describe an innovative…

The two main notions of control in quantum programming languages are often referred to as "quantum" control and "classical" control. With the latter, the control flow is based on classical information, potentially resulting from a quantum…

In the 2013 Advent calender of the Berlin Mathematics Research Center MATH+, Gerhard Woeginger presents a novel hat problem with an uncommon initial announcement. Although the information given is insufficient for the hat bearers to learn…

Impure simplicial complexes are a powerful tool to model multi-agent epistemic situations where agents may die, but it is difficult to define a satisfactory semantics for the ordinary propositional modal language on such models, since many…

Simulation and refinement are variations of the bisimulation relation, where in the former we keep only atoms and forth, and in the latter only atoms and back. Quantifying over simulations and refinements captures the effects of information…

Modal probabilistic logics provide a framework for reasoning about probability in modal contexts, involving notions such as knowledge, belief, time, and action. In this paper, we study a particular family of these logics, extending the…

We discuss winning possibilities of players in various variants of cops and robber game played on large random graphs, a testbed for various kinds of network queries, search problems in particular. We explore the use of logic frameworks to…