Val Tannen, University of Pennsylvania
First-Order Logic (FOL) model checking is the computational problem of deciding, given an FO finite model (structure) A and an FO sentence s, whether s holds true in A or not. Its provenance analysis determines how that answer (holds or not) depends on the information that defines the model A. Provenance questions like this one have emerged in databases, scientific workflows, networks, and other areas.
We apply the semiring provenance framework, developed in databases, to the FOL model checking problem. This provides a non-standard semantics for FOL that refines logical truth to values in commutative semirings: the 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 also provides an approach to negative (a.k.a. why-not or non-answers) provenance.
Joint work with Erich Grädel, RWTH Aachen University.
Val Tannen, University of Pennsylvania
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. He worked for a time in Programming Languages, and his current research interests are in Databases. 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, the management of uncertain information and algorithmic provisioning for what-if analysis. Tannen is an ACM Fellow.
author = {Val Tannen},
title = {Provenance Analysis for {First-Order} Model Checking},
year = {2019},
address = {Philadelphia, PA},
publisher = {USENIX Association},
month = jun
}