LFCS Seminar: Tuesday, 11 October 2022 - Val Tannen

Title: Provenance Analysis for First-order Model Checking

Abstract: 

Is a given finite structure a model of a given first-order sentence? The provenance analysis of this question determines how its answer depends on the atomic facts that determine the structure. Provenance questions like this one have emerged in databases, scientific workflows, networks, formal verification, and other areas.  In joint work with Erich Grädel (RWTH Aachen University) we extend the semiring provenance framework, developed in databases, to the first-order model checking problem. This provides a non-standard semantics for first-order logic that refines logical truth to values in commutative semirings: a semiring of provenance polynomials, the Viterbi semiring of confidence scores, access control semirings, etc. The semantics can be used to synthesize models based on criteria like maximum confidence or public access. Our uniform treatment of logical negation can be used to explain missing answers for queries, and failures of integrity constraints, as well as to compute corresponding repairs that fix these issues.  Time permitting, we might discuss the extension of this provenance framework to fixpoint logic (i.e., first-order logic enriched with least and greatest fixed points). Other collaborators: Mathias Naaf (RWTH Aachen University), Abdu Alawini (U Illinois), Jane Xu, and Waley Zhang (UPenn).

Bio:

Val Tannen is a professor in the Department of Computer and Information Science of the University of Pennsylvania. He joined Penn after receiving his PhD from the Massachusetts Institute of Technology in 1987.  After working for a time in Programming Languages, his current research interests are in Databases. Moreover, he has always been interested in applications of Logic to Computer Science and since 1994 he has also worked in Bioinformatics, leading a number of interdisciplinary projects.  In Databases, he and his students and collaborators have worked on query language design and on models and systems for query optimization, parallel query processing, and data integration. More recently their work has focused on models and systems for data sharing, data provenance, what-if analysis and the management of uncertain information. Tannen has received the 20 year Test-of-Time Award from ICDT and the 10 year Test-of-Time Mendelzon Award from PODS. He is an ACM Fellow.

Val Tannen's visit to the University of Edinburgh is funded by the Huawei Distinguished Visitor Programme.