计算机科学中的逻辑

We analyse the complexity of the satisfiability problem ssmSAT for State Space Models (SSM), which asks whether an input sequence can lead the model to an accepting configuration. We find that ssmSAT is undecidable in general, reflecting…

Reactive synthesis addresses the problem of generating a controller for a temporal specification in an adversarial environment; it was typically studied for LTL. Driven by applications ranging from AI to business process management, LTL…

Lightweight validation technique, such as those based on random testing, are sometimes practical alternatives to full formal verification -- providing valuable benefits, such as finding bugs, without requiring a disproportionate effort. In…

Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we…

We present a family of paraconsistent counterparts of the constructive modal logic CK. These logics aim to formalise reasoning about contradictory but non-trivial propositional attitudes like beliefs or obligations. We define their…

Partial correctness of imperative or functional programming divides in logic programming into two notions. Correctness means that all answers of the program are compatible with the specification. Completeness means that the program produces…

Classical models of computation have been successful in capturing the very essence of individual computing devices. Although they are useful to understand computability power and limitations in the small, such models are not suitable to…

We present Uppaal Coshy, a tool for automatic synthesis of a safety strategy -- or shield -- for Markov decision processes over continuous state spaces and complex hybrid dynamics. The general methodology is to partition the state space and…

Dependence logic is a formalism that augments the syntax of first-order logic with dependence atoms asserting that the value of a variable is determined by the values of some other variables, i.e., dependence atoms express functional…

Equational Theories Project is a collaborative effort, which explores the validity of certain first-order logic implications of certain kind. The project has been completed but triggered further research. This report investigates how much…

We present a complete set of rewrite rules for n-qutrit Clifford circuits where n is any non-negative integer. This is the first completeness result for any fragment of quantum circuits in odd prime dimensions. We first generalize…

We consider the problem of satisfiability of sets of constraints in a given set of finite uniform hypergraphs. While the problem under consideration is similar in nature to the problem of satisfiability of constraints in graphs, the…

We weaken the notion of "not subject to occur-check" (NSTO), on which most known results on avoiding the occur-check in logic programming are based. NSTO means that unification is performed only on such pairs of atoms for which the…

Programs that combine I/O and countable probabilistic choice, modulo either bisimilarity or trace equivalence, can be seen as describing a probabilistic strategy. For well-founded programs, we might expect to axiomatize bisimilarity via a…

Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLfp and PPLTLp, which allow to use finite-trace LTLf/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. In this…

Classical Petri nets provide a canonical model of concurrency, with unfolding semantics linking nets, occurrence nets, and event structures. No comparable framework exists for quantum concurrency: existing ''quantum Petri nets'' lack…

Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While functional correctness has seen substantial progress,…

It is well known that the reachability problem for simply-typed lambda calculus with recursive definitions and finite base-type values (finitary PCF) is decidable. A recent paper by Dal Lago and Ghyselen has shown that the same problem…

During the past decade of continuous development, the theorem prover Vampire has become an automated solver for the combined theories of commonly-used data structures. Vampire now supports arithmetic, induction, and higher-order logic.…

This paper motivates the views that for complex systems, risk should be controlled by enforcing constraints in a modular way at different system levels, that the constraints can be expressed as assurance contracts and that acceptable risk…