@MASTERSTHESIS\{IMM2007-05123,
    author       = "F. Yang",
    title        = "Static Analysis of Stochastic Process Algebras",
    year         = "2007",
    keywords     = "{PEPA,} Date Flow Analysis, Control Structure, Finite Automaton, Deadlock, Static Analysis, Stochastic Process Algebra",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Prof. Hanne Riis Nielson, {IMM,} {DTU}.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5123-full.html",
    abstract     = "The Performance Evaluation Process Algebra, {PEPA,} is introduced by Jane Hillston as a stochastic process algebra for modelling distributed systems and especially suitable for performance evaluation. A range of tools has already been developed that apply this algebra to various application areas for different purposes.

In this thesis, we present a static analysis more precisely approximating the control structure of processes expressed in {PEPA}. The analysis technique we adopted is Data Flow Analysis which is often associated with the efficient implementation of classical imperative programming languages. We begin the analysis by defining an appropriate transfer function, then with the classical worklist algorithm we construct a finite automaton that captures all possible interactions among processes. With the help of the novel methodology of annotating label and layer to the {PEPA} program, the approximating result is very precise.

Later we try to accelerate the analysis by two approaches, and develop algorithms for validating the deadlock property of the {PEPA} program. In addition, the thesis comes out with a tool that fully implements the analyses and it could be used to verify the deadlock property of the {PEPA} programs in a certain scale."
}