Model checking of infinite-state, branching-time systems and specifications

• Applicant: Dr. Harald Fecher
• Subject Area: Theoretical Computer Science
• Term: from 2006 to 2008
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 30573705

Model checking transition systems with formulas of the modal mu-calculus is an expressive and general setting for branching-time property verification of systems. Scalability benefits from abstracting transition systems prior to such checks. Predicate abstraction emerged as a key abstraction technique in safety and termination verification tools and has also been developed for 3-valued settings, all by exploiting theorem provers for the automated synthesis of abstract models. Predicate abstraction benefits from the ability to incrementally refine abstractions within the methodology of counterexample-guided abstraction refinement. The aim of this project is to improve 3-valued predicate abstraction verification of branching time systems and specifications, including the support of counterexample guided abstraction refinement. In particular, ranking functions are used to obtain complete abstraction techniques in the sense that for all infinite-state Kripke structures satisfying a formula there is a finite-state abstraction that witnesses this fact.

• DFG Programme: Research Fellowships
• International Connection: United Kingdom
• Host: Dr. Michael Huth