计算机科学中的逻辑

Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical…

Term rewriting plays a crucial role in software verification and compiler optimization. With dozens of highly parameterizable techniques developed to prove various system properties, automatic term rewriting tools work in an extensive…

The number of quantifiers needed to express first-order (FO) properties is captured by two-player combinatorial games called multi-structural games. We analyze these games on binary strings with an ordering relation, using a technique we…

The concrete security paradigm aims to give precise bounds on the probability that an adversary can subvert a cryptographic mechanism. This is in contrast to asymptotic security, where the probability of subversion may be eventually small,…

Kleisli categories have long been recognised as a setting for modelling the linear behaviour of various types of systems. However, the final coalgebra in such settings does not, in general, correspond to a fixed notion of linear semantics.…

This paper introduces AFDL, a logic-based framework for reasoning about safety, security, and defense interactions in Attack-Fault-Defense Trees, which is a model that captures all safety, security, and defense domains in a single…

Abduction is the task of computing a sufficient extension of a knowledge base (KB) that entails a conclusion not entailed by the original KB. It serves to compute explanations, or hypotheses, for such missing entailments. While this task…

Consequence-based reasoning can be used to construct proofs that explain entailments of description logic (DL) ontologies. In the literature, one can find multiple consequence-based calculi for reasoning in the $\mathcal{EL}$ family of DLs,…

Signal Temporal Logic (STL) is a widely recognized formal specification language to express rigorous temporal requirements on mixed analog signals produced by cyber-physical systems (CPS). A relevant problem in CPS design is how to…

The foundational concepts of semantic numeration systems theory are briefly outlined. The action of cardinal semantic operators unfolds over a set of cardinal abstract entities belonging to the cardinal semantic multeity. The cardinal…

Is it possible to write significantly smaller formulae when using Boolean operators other than those of the De Morgan basis (and, or, not, and the constants)? For propositional logic, a negative answer was given by Pratt: formulae over one…

The Church Problem asks for the construction of a procedure which, given a logical specification A(I,O) between input omega-strings I and output omega-strings O, determines whether there exists an operator F that implements the…

An open stochastic system \`a la Jan Willems is a system affected by two qualitatively different kinds of uncertainty: one is probabilistic fluctuation, and the other one is nondeterminism caused by a fundamental lack of information. We…

Mixed-choice has long been barred from models of asynchronous communication since it compromises the decidability of key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from…

We study Boolean classification problems over relational background structures in the logical framework introduced by Grohe and Tur\'an (TOCS 2004). It is known (Grohe and Ritzert, LICS 2017) that classifiers definable in first-order logic…

We propose a novel approach to satisfiability checking of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). CHC-based automated verification has gained considerable attention in recent years, leading to the development of…

Stream-based monitoring is a well-established runtime verification approach which relates input streams, representing sensor readings from the monitored system, with output streams that capture filtered or aggregated results. In such…

We introduce a new formalism for representing proofs in propositional logic called "scroll nets". Its fundamental construct is the "scroll", a topological notation for implication proposed by C. S. Peirce at the end of the 19th century as…

The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from a quantale. This framework provides a robust foundation for…

In \cite{sp25}, continuous information frames were introduced that capture exactly all continuous domains. They are obtained from the information frames considered in \cite{sp21} by omitting the conservativity requirement. Information…