计算机科学中的逻辑

We introduce $(\varepsilon, \delta)$-bisimulation, a novel type of approximate probabilistic bisimulation for continuous-time Markov chains. In contrast to related notions, $(\varepsilon, \delta)$-bisimulation allows the use of different…

We introduce a bisimulation learning algorithm for non-deterministic transition systems. We generalise bisimulation learning to systems with bounded branching and extend its applicability to model checking branching-time temporal logic,…

We discuss an infinitary refinement type system for input-output temporal specifications of functions that handle infinite objects like streams or infinite trees. Our system is based on a reformulation of Bonsangue and Kok's infinitary…

This paper provides a compositional approach to Taylor expansion, in the setting of cartesian differential categories. Taylor expansion is captured here by a functor that generalizes the tangent bundle functor to higher order derivatives.…

Markov decision processes (MDPs) describe sequential decision-making processes; MDP policies return for every state in that process an advised action. Classical algorithms can efficiently compute policies that are optimal with respect to,…

This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges…

Lean is an increasingly popular proof assistant based on dependent type theory. Despite its success, it still lacks important automation features present in more seasoned proof assistants, such as the Sledgehammer tactic in Isabelle/HOL. A…

We prove several negative results about first-order transducibility for classes of sparse graphs: - for every $t \in \mathbb{N}$, the class of graphs of treewidth at most $t+1$ is not transducible from the class of graphs of treewidth at…

Despite its prevalence, probabilistic bisimilarity suffers from a lack of robustness under minuscule perturbations of the transition probabilities. This can lead to discontinuities in the probabilistic bisimilarity distance function,…

State-of-the-art Boolean satisfiability (SAT) solvers constitute a practical and competitive approach for solving various real-world problems. To encourage their widespread adoption, the relatively high barrier of entry following from the…

This paper presents a new refutation procedure for multimodular systems of integer constraints that commonly arise when verifying cryptographic protocols. These systems, involving polynomial equalities and disequalities modulo different…

Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges arise in the presence of binders, freshness conditions and…

This paper investigates the view that digital hypercomputing is a good reason for rejection or re-interpretation of the Church-Turing thesis. After suggestion that such re-interpretation is historically problematic and often involves attack…

We present a propositional logic with fundamental probabilistic semantics, in which each formula is given a real measure in the interval $[0,1]$ that represents its degree of truth. This semantics replaces the binarity of classical logic,…

We provide a generic decision procedure for energy games with energy-bounded attacker and reachability objective, moving beyond vector-valued energies and vector-addition updates. All we demand is that energies form well-founded bounded…

Concurrent parameterized games involve a fixed yet arbitrary number of players. They are described by finite arenas in which the edges are labeled with languages that describe the possible move combinations leading from one vertex to…

In the Nelson-Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and the other has to satisfy a similar yet weaker property; in…

Stream-based runtime monitors are safety assurance tools that check at runtime whether the system's behavior satisfies a formal specification. Specifications consist of stream equations, which relate input streams, containing sensor…

Simulations and bisimulations are ubiquitous in the study of concurrent systems and modal logics of various types. Besides classical relational transition systems, relevant system types include, for instance, probabilistic, weighted,…

The IC3 algorithm, also known as PDR, is a SAT-based model checking algorithm that has significantly influenced the field in recent years due to its efficiency, scalability, and completeness. It utilizes SAT solvers to solve a series of SAT…