Model Checking for a Class of Performance Properties of Fluid Stochastic Models

L.M. Bujorianu, M.C. Bujorianu

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    5 Citations (Scopus)


    Recently, there is an explosive development of fluid approa- ches to computer and distributed systems. These approaches are inherently stochastic and generate continuous state space models. Usually, the performance measures for these systems are defined using probabilities of reaching certain sets of the state space. These measures are well understood in the discrete context and many efficient model checking procedures have been developed for specifications involving them. The continuous case is far more complicated and new methods are necessary. In this paper we propose a general model checking strategy founded on advanced concepts and results of stochastic analysis. Due to the problem complexity, in this paper, we achieve the first necessary step of characterizing mathematically the problem. We construct upper bounds for the performance measures using Martin capacities. We introduce a concept of bisimulation that preserves the performance measures and a metric that characterizes the bisimulation.
    Original languageUndefined
    Title of host publicationThird European Performance Engineering Workshop (EPEW)
    EditorsA. Horváth, M. Telek
    Place of PublicationBerlin
    Number of pages15
    ISBN (Print)3-540-35362-3
    Publication statusPublished - 2006
    EventThird European Performance Engineering Workshop (EPEW), Budapest, Hungary: Formal Methods and Stochastic Models for Performance Evaluation - Berlin
    Duration: 21 Jun 200622 Jun 2006

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceThird European Performance Engineering Workshop (EPEW), Budapest, Hungary


    • EWI-6965
    • MSC-68U01
    • Capacity
    • Bisimulation
    • Fluid models
    • IR-63442
    • Computer Networks
    • Markov Processes
    • Performance measure
    • METIS-238185
    • Model Checking

    Cite this