Deciding Reachability over Infinite Graphs

Speaker

Stefan Schulz, Chair of Computer Science 7
Title Deciding Reachability over Infinite Graphs
When 17.12.2008, 15.00 Uhr
Where Lecture Room Informatik 11
Abstract The general task in verification is to check whether a given (possibly infinite) system or structure satisfies a given specification. The specification is usually expressed by a logical formula. A fundamental logical formalism is first-order (FO) predicate logic. A weakness of FO logic is that reachability properties, which are important in verification, are not definable. To overcome this problem, one can extend FO logic with reachability predicates. In this talk I will present methods to generate infinite structures on which such extensions of FO logic are decidable. The techniques are based on transformations of models that preserve the decidability of logical theories. This allows to transfer known decidability results for a stronger logic (namely monadic second-order logic) to FO logic with reachability predicates on the class of transformed structures.
Slides download