Institute of Computer Science

LTG

News and Events

LTG SEMINAR, THURSDAY, DECEMBER 05, AT 13:30 IN ROOM A97 EXWI BUILDING

Antonis Achilleos: A Guide to Monitorability

I will present recent work on runtime monitorability. Runtime Verification (RV) is the technique of using a monitor to detect the violation or satisfaction of a property at runtime. One question that we ask is what properties we can monitor for. But even before giving an answer, we must first understand what that question means. Although many monitorability definitions exist, few are defined explicitly in terms of the operational guarantees provided by monitors, ie, the computational entities carrying out the verification. We view monitorability as a spectrum, where the fewer guarantees that are required of monitors, the more properties become monitorable. Accordingly, we present a monitorability hierarchy based on this trade-off. For regular, linear-time specifications, we give syntactic characterisations of the hierarchy in Hennessy-Milner logic with recursion. We then compare the obtained fragments with previous results for the branching-time setting. This is joint work with Luca Aceto, Adrian Francalanza, Anna Ingólfsdóttir, and Karoliina Lehtinen.

LTG SEMINAR, THURSDAY, NOVEMBER 28, AT 13:30 IN ROOM A97 EXWI BUILDING

Mladen Vukovic: Interpretability logic

The interpretability logic IL results from the provability logic GL (Goedel-Loeb), by adding the binary modal operator $\triangleright.$ The language of the interpretability logic contains propositional letters $p_0 , \ p_1, \ldots ,$ the logical connectives $\wedge, \ \vee , \rightarrow$ \ and \ $\neg ,$ and the unary modal operator $\Box$ and the binary modal operator \ $\triangleright .$ The axioms of the interpretability logic {\bf IL} are: all tautologies of the propositional calculus, $\Box (A\rightarrow B)\rightarrow (\Box A\rightarrow \Box B),$ \ $\Box A\rightarrow \Box \Box A,$ \ $\Box (\Box A\rightarrow A)\rightarrow \Box A,$ \ $\Box (A\rightarrow B)\rightarrow (A\triangleright B),$ \ $(A\triangleright B \ \wedge B\triangleright C)\rightarrow (A\triangleright C),$ \ $((A\triangleright C) \wedge (B\triangleright C)) \rightarrow ((A\vee B)\triangleright C),$ \ $(A\triangleright B)\rightarrow (\diamondsuit A \rightarrow \diamondsuit B),$ and \ $\diamondsuit A \triangleright A,$ where $\diamondsuit$ stands for $\neg \Box \neg$ and $\triangleright$ has the same priority as $\rightarrow .$ The deduction rules of \texttt{\bf IL} are modus ponens and necessitation. The system IL is natural from the modal point of view, but arithmetically incomplete. Various extensions of IL are obtained by adding some new axioms. These new axioms are called the principles of interpretability. We denote by ILX the system obtained by adding a principle X to the system IL. The system ILM is the interpretability logic of Peano arithmetic. The system ILP is the interpretability logic of nite axiomatizable theories. There are many principles of interpretability. We will consider the following problems on interpretability logics: semantics, completeness, fi ltration, nite model property, decidability and complexity.

LTG SEMINAR, THURSDAY, OCTOBER 31, AT 14:00 IN ROOM A97 EXWI BUILDING

Roman Kuznets: Causality in the Age of Fake News

As recently formulated by Yoram Moses, actions are not based on facts but rather on our knowledge of facts. This Knowledge of Preconditions Principle (KoP) underscores the central role that knowledge plays in decision making. The propagation of information in asynchronous in asynchronous distributed systems, i.e., those where agents do not have access to a global synchronized clock, has been well studied. It can rely solely on chains of messages, which form what Leslie Lamport called a causal cone. Until recently, this causality analysis existed only for fault-free systems and systems with very restricted types of faults. In our talk, we generalize the concept of the causal cone to systems with arbitrary byzantine failures and extract necessary conditions for achievable states of knowledge in fault-tolerant distributed systems.

LTG SEMINAR, THURSDAY, APRIL 11, AT 09:30 IN ROOM A97 EXWI BUILDING

Ioannis Kokkinis: The Dynamic Complexity of Acyclic Conjunctive Queries

Conjunctive queries (CQs) are a simple but important class of first-order definable queries. They correspond to SELCT-PROJECT-JOIN SQL queries, so they are part of almost every database query language. The importance of this class of queries is also demonstrated by the fact that the evaluation problem for CQs is a generalisation of several important problems in computer science, like the Graph Homomorphism Problem or the Boolean Satisfiability Problem. While the evaluation problem for CQs is in general NP-complete, there are interesting special cases of this problem that admit very fast algorithms (both in theory and in practise). For example the combined complexity (that means when both the CQ and the database are part of the input) of the evaluation problem for acyclic conjunctive queries (ACQs) is extremely low (it lies in the class LOGCFL, which means that it can be solved in polylogarithmic parallel time). The same holds for determining whether a CQ is acyclic. In this talk we study the combined complexity for the evaluation problem in acyclic conjunctive queries from a dynamic point of view. The goal of dynamic complexity is to determine the minimum resources needed for maintaining the answer to a problem when the input changes dynamically. An important dynamic complexity class is the class DynFO which contains all problems that can be maintained using first order formulas after single tuple insertions and deletions into/from the input. We show that the result of the evaluation of an ACQ can be maintained in DynFO after insertions and deletions of atoms into/from the query and also that it is very unlikely that the evaluation result of an ACQ can be maintained in DynFO after both changes in the database and the query. Finally we show that determining whether a query is acyclic can also be maintained in DynFO.

LTG Seminar, Thursday, April 11, at 9:30 in room A97 ExWi Building

Stepan Kuznetsov: Divide and Iterate

In this talk we briefly survey previously known and new results on the complexity, elements of proof theory, and algebraic semantics of action logic, that is, the (in)equational theory of residuated Kleene lattices, and its fragments. We emphasize the fact that adding division operations, i.e., moving from Kleene algebras to residuated ones, changes things dramatically. Namely, the systems become undecidable, and induction-based axiomatizations of iteration (Kleene star) become incomplete.

LTG Seminar, Thursday, April 11, at 9:30 in room A97 ExWi Building

Tomáš Nagy: Selfdistributive quasigroups

Selfdistributive quasigroups are interesting examples of non-associative algebraical structures. Even though the concept of selfdistributivity (e.g. the identity a*(b*c) = (a*b)*(a*c)) might sound abstract, it has interesting applications in low-dimensional topology and in many other areas of mathematics. After introducing the basic concepts, we will focus on non-affine seldistributive quasigroups, e.g. those that are not polynomially equivalent to some module. We will explain the reasons why it is not easy to classify them and we will introduce the first example of such a quasigroup that was introduced by Onoi in the year 1970. At the end, we will show a generalization of this construction that allows us to construct such quasigroups of size 2^k for all k > 5 (except for 7). We will also introduce the concept of central extensions that transforms the problem of finding non-affine selfdistributive quasigroups into solving system of linear equations over some abelian group.