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)

Abstract

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
PublisherSpringer
Pages93-107
Number of pages15
ISBN (Print)3-540-35362-3
DOIs
Publication statusPublished - 2006

Publication series

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

Keywords

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

Cite this

Bujorianu, L. M., & Bujorianu, M. C. (2006). Model Checking for a Class of Performance Properties of Fluid Stochastic Models. In A. Horváth, & M. Telek (Eds.), Third European Performance Engineering Workshop (EPEW) (pp. 93-107). [10.1007/11777830_7] (Lecture Notes in Computer Science; Vol. 4054, No. 2). Berlin: Springer. https://doi.org/10.1007/11777830_7
Bujorianu, L.M. ; Bujorianu, M.C. / Model Checking for a Class of Performance Properties of Fluid Stochastic Models. Third European Performance Engineering Workshop (EPEW). editor / A. Horváth ; M. Telek. Berlin : Springer, 2006. pp. 93-107 (Lecture Notes in Computer Science; 2).
@inproceedings{0118ee92550b47adba8a46fba234f907,
title = "Model Checking for a Class of Performance Properties of Fluid Stochastic Models",
abstract = "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.",
keywords = "EWI-6965, MSC-68U01, Capacity, Bisimulation, Fluid models, IR-63442, Computer Networks, Markov Processes, Performance measure, METIS-238185, Model Checking",
author = "L.M. Bujorianu and M.C. Bujorianu",
note = "10.1007/11777830_7",
year = "2006",
doi = "10.1007/11777830_7",
language = "Undefined",
isbn = "3-540-35362-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
number = "2",
pages = "93--107",
editor = "A. Horv{\'a}th and M. Telek",
booktitle = "Third European Performance Engineering Workshop (EPEW)",

}

Bujorianu, LM & Bujorianu, MC 2006, Model Checking for a Class of Performance Properties of Fluid Stochastic Models. in A Horváth & M Telek (eds), Third European Performance Engineering Workshop (EPEW)., 10.1007/11777830_7, Lecture Notes in Computer Science, no. 2, vol. 4054, Springer, Berlin, pp. 93-107. https://doi.org/10.1007/11777830_7

Model Checking for a Class of Performance Properties of Fluid Stochastic Models. / Bujorianu, L.M.; Bujorianu, M.C.

Third European Performance Engineering Workshop (EPEW). ed. / A. Horváth; M. Telek. Berlin : Springer, 2006. p. 93-107 10.1007/11777830_7 (Lecture Notes in Computer Science; Vol. 4054, No. 2).

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

TY - GEN

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

AU - Bujorianu, L.M.

AU - Bujorianu, M.C.

N1 - 10.1007/11777830_7

PY - 2006

Y1 - 2006

N2 - 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.

AB - 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.

KW - EWI-6965

KW - MSC-68U01

KW - Capacity

KW - Bisimulation

KW - Fluid models

KW - IR-63442

KW - Computer Networks

KW - Markov Processes

KW - Performance measure

KW - METIS-238185

KW - Model Checking

U2 - 10.1007/11777830_7

DO - 10.1007/11777830_7

M3 - Conference contribution

SN - 3-540-35362-3

T3 - Lecture Notes in Computer Science

SP - 93

EP - 107

BT - Third European Performance Engineering Workshop (EPEW)

A2 - Horváth, A.

A2 - Telek, M.

PB - Springer

CY - Berlin

ER -

Bujorianu LM, Bujorianu MC. Model Checking for a Class of Performance Properties of Fluid Stochastic Models. In Horváth A, Telek M, editors, Third European Performance Engineering Workshop (EPEW). Berlin: Springer. 2006. p. 93-107. 10.1007/11777830_7. (Lecture Notes in Computer Science; 2). https://doi.org/10.1007/11777830_7