计算机科学中的逻辑

Finding solution values for unknowns in Boolean equations was a principal reasoning mode in the Algebra of Logic of the 19th century. Schr\"oder investigated it as Aufl\"osungsproblem (solution problem). It is closely related to the modern…

We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly,…

We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all…

We build on the theory of ontology logs (ologs) created by Spivak and Kent, and define a notion of wiring diagrams. In this article, a wiring diagram is a finite directed labelled graph. The labels correspond to types in an olog; they can…

We study the complexity of the model-checking problem for parameterized discrete-timed systems with arbitrarily many anonymous and identical processes, with and without a distinguished "controller", and communicating via synchronous…

We present a new encoding of the Battle of Hercules and Hydra as a rewrite system with AC symbols. Unlike earlier term rewriting encodings, it faithfully models any strategy of Hercules to beat Hydra. To prove the termination of our…

Weakest preconditions are a useful notion for program verification as they reduce a problem of program verification to a problem of constraint solving. Category-theoretic generalisations of weakest preconditions have been studied to capture…

In this communication, we resolve a longstanding open question in the probabilistic verification of infinite-state systems. We show that model checking {\it stateless probabilistic pushdown systems (pBPA)} against {\it probabilistic…

We present a different proof of the insecurity problem for XOR, solved in by Chevalier, Kuesters, Rusinowitch and Turuani (2005). Our proof uses the notion of typed terms and well-typed proofs, and removes a restriction on the class of…

We give a quantifier elimination procedure for one-parametric Presburger arithmetic, the extension of Presburger arithmetic with the function $x \mapsto t \cdot x$, where $t$ is a fixed free variable ranging over the integers. This resolves…

In this paper, we develop a logico-algebraic framework for modeling decision-making through deliberation in multi-agent settings. The central concept in this framework is that of interrogative agendas, which represent the cognitive stances…

Vectors addition systems with states (VASS), or equivalently Petri nets, are arguably one of the most studied formalisms for the modeling and analysis of concurrent systems. A central decision problem for VASS is reachability: whether there…

Interactive theorem provers (ITPs) are powerful tools for the formal verification of mathematical proofs down to the axiom level. However, their lack of a natural language interface remains a significant limitation. Recent advancements in…

We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although…

A famous result due to Lov\'{a}sz states that two finite relational structures $M$ and $N$ are isomorphic if, and only if, for all finite relational structures $T$, the number of homomorphisms from $T$ to $M$ is equal to the number of…

We introduce $\omega$-catoids as generalisations of (strict) $\omega$-categories and in particular the higher path categories generated by computads or polygraphs in higher-dimensional rewriting. We also introduce $\omega$-quantales that…

We study networks of processes that all execute the same finite-state protocol and communicate via broadcasts. We are interested in two problems with a parameterized number of processes: the synchronization problem which asks whether there…

We relate the so-called powercone models of mixed non-deterministic and probabilistic choice proposed by Tix, Keimel, Plotkin, Mislove, Ouaknine, Worrell, Morgan, and McIver, to our own models of previsions. Under suitable topological…

String diagrammatic calculi have become increasingly popular in fields such as quantum theory, circuit theory, probabilistic programming, and machine learning, where they enable resource-sensitive and compositional algebraic analysis.…

In runtime verification, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace satisfies a given specification. We generalize the theory of runtime…