Model Checking Is Static Analysis of Modal Logic

Flemming Nielson, Hanne Riis Nielson

    Research output: Contribution to journalConference articleResearchpeer-review

    Abstract

    Flow Logic is an approach to the static analysis of programs that has been developed for functional, imperative and object-oriented programming languages and for concurrent, distributed, mobile and cryptographic process calculi. In this paper we extend it; to deal with modal logics and prove that it can give an exact characterisation of the semantics of formulae in a modal logic. This shows that model checking can be performed by means of state-of-the-art approaches to static analysis and allow us to conclude that the problems of model checking and static analysis are reducible to each other. In terms of computational complexity we show that model checking by means of static analysis gives the same complexity bounds as are known for traditional approaches to model checking.
    Original languageEnglish
    Book seriesLecture Notes in Computer Science
    Volume6014
    Pages (from-to)191-205
    ISSN0302-9743
    DOIs
    Publication statusPublished - 2010

    Fingerprint

    Dive into the research topics of 'Model Checking Is Static Analysis of Modal Logic'. Together they form a unique fingerprint.

    Cite this