Reachability for Finite-State Process Algebras Using Static Analysis

Nataliya Skrypnyuk, Flemming Nielson

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    In this work we present an algorithm for solving the reachability problem in finite systems that are modelled with process algebras. Our method uses Static Analysis, in particular, Data Flow Analysis, of the syntax of a process algebraic system with multi-way synchronisation. The results of the Data Flow Analysis are used in order to “cut off” some of the branches in the reachability analysis that are not important for determining, whether or not a state is reachable. In this way, it is possible for our reachability algorithm to avoid building large parts of the system altogether and still solve the reachability problem in a precise way.
    Original languageEnglish
    Title of host publicationReachability Problems : 5th InternationalWorkshop, RP 2011 Genoa, Italy, September 28-30, 2011, Proceedings
    Volume6945
    PublisherSpringer
    Publication date2011
    Pages231-244
    ISBN (Print)978-3-642-24287-8
    ISBN (Electronic)978-3-642-24288-5
    DOIs
    Publication statusPublished - 2011
    Event5th International Workshop on Reachability Problems - Genoa, Italy
    Duration: 28 Sept 201130 Sept 2011
    Conference number: 5

    Conference

    Conference5th International Workshop on Reachability Problems
    Number5
    Country/TerritoryItaly
    CityGenoa
    Period28/09/201130/09/2011
    SeriesLecture Notes in Computer Science
    ISSN0302-9743

    Keywords

    • Static analysis
    • Reachability
    • Process algebra

    Fingerprint

    Dive into the research topics of 'Reachability for Finite-State Process Algebras Using Static Analysis'. Together they form a unique fingerprint.

    Cite this