Reachability for Finite-State Process Algebras Using Static Analysis

Nataliya Skrypnyuk, Flemming Nielson

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


    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
    Publication date2011
    ISBN (Print)978-3-642-24287-8
    ISBN (Electronic)978-3-642-24288-5
    Publication statusPublished - 2011
    EventInternational Workshop on Reachability Problems - Genoa, Italy
    Duration: 1 Jan 2011 → …
    Conference number: 5


    ConferenceInternational Workshop on Reachability Problems
    CityGenoa, Italy
    Period01/01/2011 → …
    SeriesLecture Notes in Computer Science


    • Static analysis
    • Reachability
    • Process algebra


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

    Cite this