Modal abstractions of concurrent behavior

Flemming Nielson, Sebastian Nanz, Hanne Riis Nielson

    Research output: Contribution to journalJournal articleResearchpeer-review


    We present an effective algorithm for the automatic construction of finite modal transition systems as abstractions of potentially infinite concurrent processes. Modal transition systems are recognized as valuable abstractions for model checking because they allow for the validation as well as refutation of safety and liveness properties. However, the algorithmic construction of finite abstractions from potentially infinite concurrent processes is a missing link that prevents their more widespread usage for model checking of concurrent systems. Our algorithm is a worklist algorithm using concepts from abstract interpretation and operating upon mappings from sets to intervals in order to express simultaneous over- and underapprox-imations of the multisets of process actions available in a particular state. We obtain a finite abstraction that is 3-valued in both states and transitions and that supports the definition of a 3-valued modal logic for validating as well as refuting properties of systems. The construction is illustrated on a few examples, including the Ingemarsson-Tang-Wong key agreement protocol. © 2011 ACM.
    Original languageEnglish
    JournalA C M Transactions on Computational Logic
    Issue number3
    Pages (from-to)18
    Publication statusPublished - 2011

    Fingerprint Dive into the research topics of 'Modal abstractions of concurrent behavior'. Together they form a unique fingerprint.

    Cite this