Performance evaluation:= (process algebra + model checking) x Markov chains

H. Hermanns, K.G. Larsen (Editor), Mogens Nielsen (Editor), Joost P. Katoen

    Research output: Contribution to conferencePaperAcademic

    11 Citations (Scopus)
    174 Downloads (Pure)

    Abstract

    Markov chains are widely used in practice to determine system performance and reliability characteristics. The vast majority of applications considers continuous-time Markov chains (CTMCs). This tutorial paper shows how successful model specification and analysis techniques from concurrency theory can be applied to performance evaluation. The specification of CTMCs is supported by a stochastic process algebra, while the quantitative analysis of these models is tackled by means of model checking. Process algebra provides: (i) a high-level specification formalism for describing CTMCs in a precise, modular and constraint-oriented way, and (ii) means for the automated generation and aggregation of CTMCs. Temporal logic model checking provides: (i) a formalism to specify complex measures-of-interest in a lucid, compact and flexible way, (ii) automated means to quantify these measures over CTMCs, and (iii) automated measure-driven aggregation (lumping) of CTMCs. Combining process algebra and model checking constitutes a coherent framework for performance evaluation based on CTMCs.
    Original languageEnglish
    Pages59-81
    Number of pages23
    DOIs
    Publication statusPublished - 2001
    Event12th International Conference on Concurrency Theory, CONCUR 2001 - Aalborg, Denmark
    Duration: 20 Aug 200125 Aug 2001
    Conference number: 12

    Conference

    Conference12th International Conference on Concurrency Theory, CONCUR 2001
    Abbreviated titleCONCUR
    CountryDenmark
    CityAalborg
    Period20/08/0125/08/01

    Keywords

    • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
    • FMT-PM: PROBABILISTIC METHODS
    • EWI-6448
    • FMT-MC: MODEL CHECKING
    • IR-66268
    • FMT-PA: PROCESS ALGEBRAS

    Fingerprint Dive into the research topics of 'Performance evaluation:= (process algebra + model checking) x Markov chains'. Together they form a unique fingerprint.

    Cite this