ICE-TCS seminar: Elli Anastasiadi
Parameter trade-offs for the Model Checking Problem
ICE-TCS seminar #330
Date and time: Tuesday, 5 March 2019, 12:10-13:00 (note the non-standard time)
Location: Room M120
Speaker: Elli Anastasiadi (Reykjavik University)
Title: Parameter trade-offs for the Model Checking Problem.
Abstract: The model checking problem for a logic is defined as the problem of deciding, given some structure S and a formula F expressible in the logic, whether S has the property described by F. This problem is quite complex, as the property is part of the input. Starting with propositional logic and increasing our "expressive power" up to first-order logic, second-order logic and so on, the model checking problem quickly becomes NP-hard. Such hard problems are at the centre of parameterized complexity, which focuses on presenting efficient algorithms (FPT=fixed parameter tractable) for fragments of the possible input structures through the use of parameters. A combination of those two fields has already proved that the model checking problem can be efficiently solved for some logics if the input structures are restricted in some specific manner. Through the results of such attempts, it seems that there is a correlation between the expressive power of a logic and the parameter needed to classify it in FPT. This work is an attempt to generalize the trade-off between time efficiency and universality of the solution for model checking of classical logics over graph structures.
The talk builds on joint work with professor Aris Pagourtzis (National Technical University of Athens).
This talk does not assume any background on Parameterized Complexity or technical knowledge on Logic and Model Checking. However, some familiarity with such fields will ensure a better understanding of the project.
