Seminar talks fall 2019
Talks during the fall term 2019
Wed 4.9.2019 12-14, C124
Joni Puljujärvi: Scott sentences of metric structures in infinitary continuous logic
Wed 11.9.2019 12-13, C124
Bernd Finkbeiner (Universität des Saarlandes): Logics and Algorithms for the Synthesis of Distributed Systems
Abstract: Sixty years after its introduction by Alonzo Church, the synthesis problem is still one of the most intriguing challenges in the theory of discrete systems. On the one hand, synthesis algorithms have found game-changing applications in many areas of computer science and systems engineering, from the automatic construction of control strategies for robots and manufacturing plants to the computer-aided design of coordination protocols and human-computer interfaces. On the other hand, the logical and algorithmic foundations of the synthesis problem are far from complete.
Synthesis is particularly difficult in the setting of distributed systems, where we try to find a combination of process implementations that jointly guarantee that a given specification is satisfied. A reduction from multi-player games shows that the problem is in general undecidable. Despite this negative result, there is a long history of discoveries where the decidability of the synthesis problem was established for distributed systems with specific architectures, such as pipelines and rings, or other restrictions on the problem, such as local specifications. Encouraged by these findings, new specification languages like Coordination Logic aim for a comprehensive logical representation and a uniform algorithmic treatment of the decidable synthesis problems.
In this talk, I will trace the progress from isolated decidability results towards universal synthesis logics and algorithms. I will demonstrate how the logical representation of the synthesis problem simplifies the identification of decidable cases and give an overview on the state of the art in decision procedures and strategy construction algorithms for the synthesis of distributed systems.
Wed 18.9.2019 12-14, C124
No seminar
Wed 25.9.2019 12-14, C124
Davide Quadrellaro: Lattices of DNA logics and applications to Inquisitive Logic
Wed 2.10.2019 12-14, C124
Tapani Hyttinen: On discrete approximations of Hilbert space operators
Wed 9.10.2019 12-14, C124
Keijo Heljanko: Bounded Model Checking for Weak Memory Models
Abstract: We present Dartagnan, a bounded model checker (BMC) for concurrent programs under weak memory models. Its distinguishing feature is that the memory model is not implemented inside the tool but taken as part of the input. Dartagnan reads CAT, the standard language for memory models, which allows to define x86/TSO, ARMv7, ARMv8, Power, C/C++, and Linux kernel concurrency primitives. BMC with memory models as inputs is challenging. One has to encode into SMT not only the program but also its semantics as defined by the memory model. What makes Dartagnan scale is its relation analysis, a novel static analysis that significantly reduces the size of the encoding. Dartagnan matches or even exceeds the performance of the model-specific verification tools Nidhugg and CBMC, as well as the performance of Herd, a CAT-compatible litmus testing tool. Compared to the unoptimized encoding, the speed-up is often more than two orders of magnitude.
Wed 16.10.2019 12-14, C124
Jeremias Berg: Bounded Treewidth Bayesian Network Structure Learning with Maximum Satisfiability
Wed 23.10.2019 12-14, C124
exam week
Wed 30.10.2019 12-14, C124
Anssi Yli-Jyrä: Embedding Graphs to the String Space to Support Succinct Representation of Graph Properties
Abstract: Classical formal language theory concerns subsets of a finitely generated free monoid. In this presentation, I define the universe of graphs as an infinitely generated free monoid, whose generator has a string representation as an indexed language. I also show that a particularly bounded height-deterministic context-free subset represents a generator for a proper superset of the crossing graphs and that a more bounded regular subset represents a generator that is sufficient for representing observed dependency trees of natural language syntax as strings. Such embedding of graphs to height-deterministic languages suggests that efficiently decidable fragments of monadic second-order logic over graphs could be pursued and implemented via the closure properties of height-deterministic context-free languages.
These results are implied by my recent paper that forms the core of the presentation. The paper is called "Transition-Based Coding and Formal Language Theory for Ordered Digraphs" and it is online. Its abstract reads:
Transition-based parsing of natural language uses transition systems to build directed annotation graphs (digraphs) for sentences. In this paper, we define, for an arbitrary ordered digraph, a unique decomposition and a corresponding linear encoding that are associated bijectively with each other via a new transition system. These results give us an efficient and succinct representation for digraphs and sets of digraphs. Based on the system and our analysis of its syntactic properties, we give structural bounds under which the set of encoded digraphs is restricted and becomes a context-free or a regular string language. The context-free restriction is essentially a superset of the encodings used previously to characterize properties of noncrossing digraphs and to solve maximal subgraphs problems. The regular restriction with a tight bound is shown to capture the Universal Dependencies v2.4 treebanks in linguistics.
Tue 5.11.2019 10-12, D123
Alessio Mansutti (CNRS, LSV, ENS Paris-Saclay): Internal calculi for Separation Logic
Abstract: Separation Logic (SL) is a well-known assertion logic providing a scalable solution for Hoare-style verification of imperative, heap-manipulating programs. To achieve scalability, Separation Logic relies on two spatial connectives to represent parts of a memory region.
In the first part of this talk, we briefly recall the definition of Hoare's proof system and discuss why this formalism lacks modularity when instantiated for the verification of programs dealing with pointers. We then introduce First-Order Separation Logic (FOSL) and the computational complexity of its decision problems. Well-known fragments of this logic are also discussed. The second part of the talk is devoted to proof-systems for SL. After showing that FOSL cannot be recursively axiomatised, we present the first proof-system for Quantifier-free SL. In order to deal with the two spatial connectives, we examine the logic from a model theoretic point of view. We find a syntactical fragment CORE whose complexity is equivalent to the whole logic, but where spatial connectives can be used in a very restrictive way. A sound and complete axiomatisation of Quantifier-free SL is then obtained by defining axioms and rules that translate every formula to CORE, together with an axiom system for this fragment. The work on axiomatisation is done jointly with S. Demri (CNRS, LSV, ENS Paris-Saclay) and E. Lozes (I3S, Université côte d´Azur), and will be presented at CSL’20.
Stéphane Demri (CNRS, LSV, ENS Paris-Saclay): Modal Separation Logics and Friends
Abstract: Separation logic is known as an assertion language to perform verification, by extending Hoare-Floyd logic in order to verify programs with mutable data structures. The separating conjunction allows us to evaluate formulae in subheaps, and this possibility to evaluate formulae in alternative models is a feature shared with many modal logics such as sabotage logics, logics of public announcements or relation-changing modal logics. In the first part of the talk, we present several versions of modal separation logics whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction. Fragments are genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. In the second part of the talk, we present the decidability status and the computational complexity of modal separation logics, (for instance, leading to NP-complete or Tower-complete satisfiability problems). In the third part, we investigate the Hilbert-style axiomatisation of several modal separation logics. Part of the presented work is done jointly with R. Fervari (U. of Cordoba) and A. Mansutti (LSV, ENS Paris-Saclay).
Wed 13.11.2019 12-14, C124
Max Sandström : Safety and Liveness of Hyperproperties
Wed 20.11.2019 12-14, C124
Fausto Barbero: Strong undefinability of connectives in inquisitive semantics
Wed 27.11.2019 12-14, C124
Tapio Saarinen: The group extension problem and group cohomology: a peek at homological algebra
Wed 4.12.2019 12-14, C124
Otto Rajala: Characterization of an inner model from cofinality logic assuming V=L[U]
Wed 11.12.2019 12-14, C124
Antti Kuusisto: Counting models
Abstract: The model counting problem takes as an input a sentence Phi and an integer n, outputting the number of n-element models of Phi; the domain of the models is taken to be {1,...,n} while the signature is the signature of Phi. We discuss some fundamental issues relating to this fundamental problem.
Wed 18.12.2019 12-14, C124
exam week