Symbolic Semantics and Verification of Stochastic Process Algebras

G.W.M. Kuntz

    Research output: ThesisPhD Thesis - Research UT, graduation external

    21 Downloads (Pure)

    Abstract

    In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: 1) State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). 2) The specification and automatic verification of complex system requirements This thesis contributes to the alleviation of the state space explosion problem by devising a new denotational semantics for stochastic process algebras that relies on efficient data structures for the compact representation of even huge state spaces. The second problem is addressed by devising a new stochastic temporal logic and corresponding verification algorithms, that allow the sepcification and verification of complex system requirements.
    Original languageUndefined
    Awarding Institution
    • University of Erlangen-Nuremberg
    Supervisors/Advisors
    • Leipertz, Alfred, Supervisor
    • Siegle, Markus, Supervisor
    • German, Reinhard, Supervisor
    Thesis sponsors
    Award date2 Feb 2006
    Place of PublicationErlangen
    Publisher
    Publication statusPublished - 2 Feb 2006

    Keywords

    • IR-63897
    • METIS-238735
    • EWI-8963

    Cite this

    Kuntz, G. W. M. (2006). Symbolic Semantics and Verification of Stochastic Process Algebras. Erlangen: Springer.
    Kuntz, G.W.M.. / Symbolic Semantics and Verification of Stochastic Process Algebras. Erlangen : Springer, 2006. 240 p.
    @phdthesis{12f736573a704bd880d4e4f3f126b7bc,
    title = "Symbolic Semantics and Verification of Stochastic Process Algebras",
    abstract = "In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: 1) State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). 2) The specification and automatic verification of complex system requirements This thesis contributes to the alleviation of the state space explosion problem by devising a new denotational semantics for stochastic process algebras that relies on efficient data structures for the compact representation of even huge state spaces. The second problem is addressed by devising a new stochastic temporal logic and corresponding verification algorithms, that allow the sepcification and verification of complex system requirements.",
    keywords = "IR-63897, METIS-238735, EWI-8963",
    author = "G.W.M. Kuntz",
    year = "2006",
    month = "2",
    day = "2",
    language = "Undefined",
    publisher = "Springer",
    school = "University of Erlangen-Nuremberg",

    }

    Kuntz, GWM 2006, 'Symbolic Semantics and Verification of Stochastic Process Algebras', University of Erlangen-Nuremberg, Erlangen.

    Symbolic Semantics and Verification of Stochastic Process Algebras. / Kuntz, G.W.M.

    Erlangen : Springer, 2006. 240 p.

    Research output: ThesisPhD Thesis - Research UT, graduation external

    TY - THES

    T1 - Symbolic Semantics and Verification of Stochastic Process Algebras

    AU - Kuntz, G.W.M.

    PY - 2006/2/2

    Y1 - 2006/2/2

    N2 - In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: 1) State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). 2) The specification and automatic verification of complex system requirements This thesis contributes to the alleviation of the state space explosion problem by devising a new denotational semantics for stochastic process algebras that relies on efficient data structures for the compact representation of even huge state spaces. The second problem is addressed by devising a new stochastic temporal logic and corresponding verification algorithms, that allow the sepcification and verification of complex system requirements.

    AB - In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: 1) State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). 2) The specification and automatic verification of complex system requirements This thesis contributes to the alleviation of the state space explosion problem by devising a new denotational semantics for stochastic process algebras that relies on efficient data structures for the compact representation of even huge state spaces. The second problem is addressed by devising a new stochastic temporal logic and corresponding verification algorithms, that allow the sepcification and verification of complex system requirements.

    KW - IR-63897

    KW - METIS-238735

    KW - EWI-8963

    M3 - PhD Thesis - Research UT, graduation external

    PB - Springer

    CY - Erlangen

    ER -

    Kuntz GWM. Symbolic Semantics and Verification of Stochastic Process Algebras. Erlangen: Springer, 2006. 240 p.