计算机科学中的逻辑

We present a theory of "quantum references", similar to lenses in classical functional programming, that allow to point to a subsystem of a larger quantum system, and to mutate/measure that part. Mutable classical variables, quantum…

Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabilistic programs. Usually, extending verification methods to…

In this work, a functional variant of the polynomial analogue of the classical Gandy's fixed point theorem is obtained. Sufficient conditions have been found to ensure that the complexity of the recursive function does not go beyond the…

Protection of confidential data is an important security consideration of today's applications. Of particular concern is to guard against unintentional leakage to a (malicious) observer, who may interact with the program and draw inference…

Time-Sensitive Distributed Systems (TSDS), such as applications using autonomous drones, achieve goals under possible environment interference (\eg, winds). Moreover, goals are often specified using explicit time constraints which must be…

The study of group knowledge concepts such as mutual, common, and distributed knowledge is well established within the discipline of epistemic logic. In this work, we incorporate epistemic abilities of agents to refine the formal definition…

Interpolation-based techniques become popular in recent years, as they can improve the scalability of existing verification techniques due to their inherent modularity and local reasoning capabilities. Synthesizing Craig interpolants is the…

Game comonads offer a categorical view of a number of model-comparison games central to model theory, such as pebble and Ehrenfeucht-Fra\"iss\'e games. Remarkably, the categories of coalgebras for these comonads capture preservation of…

We develop a learning algorithm for closed signal flow graphs - a graphical model of signal transducers. The algorithm relies on the correspondence between closed signal flow graphs and weighted finite automata on a singleton alphabet. We…

Denotational models of type theory, such as set-theoretic, domain-theoretic, or category-theoretic models use (actual) infinite sets of objects in one way or another. The potential infinite, seen as an extensible finite, requires a dynamic…

We are interested in characterizing which classes of finite graphs are well-quasi-ordered by the induced subgraph relation. To that end, we devise an algorithm to decide whether a class of finite graphs well-quasi-ordered by the induced…

Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a comprehensive overview of the Lebesgue Differentiation…

We show that (local) confluence of terminating locally constrained rewrite systems is undecidable, even when the underlying theory is decidable. Several confluence criteria for logically constrained rewrite systems are known. These were…

Earlier papers \cite{VB2022,VB2023a,VB2023b} introduced the notions of a core and an index of a relation (an index being a special case of a core). A limited form of the axiom of choice was postulated -- specifically that all partial…

The graphical modeling language GRAFCET is used as a formal specification language in industrial control design. This paper proposes a structural analysis that approximates the variable values of GRAFCET to allow verification on…

We address the problem of learning temporal properties from the branching-time behavior of systems. Existing research in this field has mostly focused on learning linear temporal properties specified using popular logics, such as Linear…

We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translatability of proofs between the two formalisms. In particular,…

Active automata learning (AAL) is a method to infer state machines by interacting with black-box systems. Adaptive AAL aims to reduce the sample complexity of AAL by incorporating domain specific knowledge in the form of (similar) reference…

This paper studies the influence of probabilism and non-determinism on some quantitative aspect X of the execution of a system modeled as a Markov decision process (MDP). To this end, the novel notion of demonic variance is introduced: For…

We present a new and powerful algebraic framework for graph rewriting, based on drags, a class of graphs enjoying a novel composition operator. Graphs are embellished with roots and sprouts, which can be wired together to form edges. Drags…