Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Provenance Analysis for Logic and Games
Speaker:Erich Grädel
coming from:RWTH Aachen
Speakers Bio:
Event Type:Talk
Visibility:D1, D2, D3, INET, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Wednesday, 31 July 2019
Duration:60 Minutes
Building:E1 4
A model checking computation checks whether a given logical

sentence is true in a given finite structure. Provenance analysis,
based on interpretations in commutative semirings, abstracts
from such a computation mathematical information on how the result
depends on the atomic data that describe the structure.

In this approach, atomic facts are interpreted not just by true
or false, but by values in an appropriate semiring, where 0 is
the value of false statements, whereas any element $a\neq 0$ of the
semiring stands for some shade of truth. These values are then
propagated from the atomic facts to arbitrary statements in the language.

In database theory, provenance analysis has been successfully developed
for positive query languages such a unions of conjunctive queries,
positive relational algebra, or datalog. However, it did not really
offer an adequate treatment of negation or missing information.

We propose a new approach for the provenance analysis of logics with
negation, such as first-order logic and fixed-point logics. It is
closely related to a provenance analysis of the associated model-checking
games, and based on new provenance semirings of polynomials and formal
power series, which take negation into account. They are obtained by
taking quotients of traditional provenance semirings by congruences
generated by products of positive and negative provenance tokens;
they are called semirings of dual-indeterminate polynomials or
dual-indeterminate power series.

Beyond the use for model-checking problems in logics, provenance
analysis of games is of independent interest. Provenance values in
games provide detailed information about the number and properties
of the strategies of the players, far beyond the question whether
or not a player has a winning strategy from a given position.

This is joint work with Val Tannen.

Name(s):Jennifer Müller
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:111
Meeting ID:N/A
Tags, Category, Keywords and additional notes
Attachments, File(s):
  • Jennifer Müller, 07/30/2019 09:47 AM
  • Jennifer Müller, 07/24/2019 02:24 PM -- Created document.