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
    EventInternational Workshop on Reachability Problems - Genoa, Italy
    Duration: 1 Jan 2011 → …
    Conference number: 5

    Conference

    ConferenceInternational Workshop on Reachability Problems
    Number5
    CityGenoa, Italy
    Period01/01/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