An abstract interpretation toolkit for μCRL

Miguel Valero Espada, Jaco van de Pol

    Research output: Contribution to journalArticleAcademicpeer-review

    5 Citations (Scopus)
    3 Downloads (Pure)

    Abstract

    This paper describes a toolkit that assists in the task of generating abstract approximations of process algebraic specifications written in the language μCRL. Abstractions are represented by Modal Labelled Transition Systems, which are mixed transition systems with may and must modalities. The approach permits to infer the satisfaction or refutation of safety and liveness properties expressed in the (action-based) μ-calculus. The tool supports the abstraction of states and action labels, which allows to deal with infinitely branching systems.
    Original languageEnglish
    Pages (from-to)249-273
    Number of pages25
    JournalFormal methods in system design
    Volume30
    Issue number3
    DOIs
    Publication statusPublished - Jun 2007

    Keywords

    • FMT-MC: MODEL CHECKING
    • Model checking
    • Process algebra
    • μCRL
    • Abstract interpretation

    Fingerprint

    Dive into the research topics of 'An abstract interpretation toolkit for μCRL'. Together they form a unique fingerprint.

    Cite this