计算机科学中的逻辑

Following our recent development of a compositional model checking algorithm for Markov decision processes, we present a compositional framework for solving mean payoff games (MPGs). The framework is derived from category theory,…

This work is a part of an ongoing effort to understand the relationships between properties used in theory combination. We here focus on including two properties that are related to shiny theories: the finite model property and stable…

In earlier work, we introduced the framework of language-based decisions, the core idea of which was to modify Savage's classical decision-theoretic framework by taking actions to be descriptions in some language, rather than functions from…

Context: Model checking has become a key tool for gaining confidence in correctness of multi-threaded programs. Unit tests and functional tests do not suffice because of race conditions that are not discovered by those tests. This problem…

We introduce the notion of a Real Equation System (RES), which lifts Boolean Equation Systems (BESs) to the domain of extended real numbers. Our RESs allow arbitrary nesting of least and greatest fixed-point operators. We show that each RES…

Automata operating on infinite objects feature prominently in the theory of the modal $\mu$-calculus. One such application concerns the tableau games introduced by Niwi\'{n}ski & Walukiewicz, of which the winning condition for infinite…

Constrained Horn Clauses (CHCs) are often used in automated program verification. Thus, techniques for (dis-)proving satisfiability of CHCs are a very active field of research. On the other hand, acceleration techniques for computing…

A foundational theory of compositional categorical rewriting theory is presented, based on a collection of fibration-like properties that collectively induce and intrinsically structure the large collection of lemmata used in the proofs of…

In online monitoring, we first synthesize a monitor from a formal specification, which later runs in tandem with the system under study, incrementally receiving its progress and evolving with the system. In offline monitoring the trace is…

Primal logic arose in access control; it has a remarkably efficient (linear time) decision procedure for its entailment problem. But primal logic is a general logic of information. In the realm of arbitrary items of information (infons),…

Linear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as the verification of probabilistic systems, model checking, computational biology, and economics. Positivity (are all terms of…

In Statistical Relational Artificial Intelligence, a branch of AI and machine learning which combines the logical and statistical schools of AI, one uses the concept {\em para\-metrized probabilistic graphical model (PPGM)} to model…

We give a comprehensive account on the parameterized complexity of model checking and satisfiability of propositional inclusion and independence logic. We discover that for most parameterizations the problems are either in FPT or…

Reactive systems \`a la Leifer and Milner, an abstract categorical framework for rewriting, provide a suitable framework for deriving bisimulation congruences. This is done by synthesizing interactions with the environment in order to…

We discuss model-checking problems as formal models of algorithmic law. Specifically, we ask for an algorithmically tractable general purpose model-checking problem that naturally models the European transport Regulation 561, and discuss…

Assuming that the term 'metaverse' could be understood as a computer-based implementation of multiverse applications, we started to look in the present work for a logic that would be powerful enough to handle the situations arising both in…

Sessions are a fundamental notion in message-passing systems. A session is an abstract notion of communication between parties where each one owns an endpoint. Session types are types that are assigned to the endpoints and that are used to…

Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where quantification over probabilistic schedulers resolves…

We study the problem of computing minimal distinguishing formulas for non-bisimilar states in finite LTSs. We show that this is NP-hard if the size of the formula must be minimal. Similarly, the existence of a short distinguishing trace is…

Encodings are the main way to compare process calculi. By applying quality criteria to encodings we analyse their quality and rule out trivial or meaningless encodings. Thereby, operational correspondence is one of the most common and most…