Simulation for continuous-time Markov chains

J. Brim (Editor), Christel Baier, Joost P. Katoen, P. Jancar (Editor), H. Hermanns, M. Kretnsk (Editor), Boudewijn R.H.M. Haverkort, A. Kucera (Editor)

Research output: Contribution to conferencePaperAcademicpeer-review

17 Citations (Scopus)
12 Downloads (Pure)

Abstract

This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.
Original languageUndefined
Pages473-489
Number of pages15
DOIs
Publication statusPublished - 2002
Event13th International Conference on Concurrency Theory, CONCUR 2002 - Brno, Czech Republic
Duration: 20 Aug 200223 Aug 2002
Conference number: 13

Conference

Conference13th International Conference on Concurrency Theory, CONCUR 2002
Abbreviated titleCONCUR
CountryCzech Republic
CityBrno
Period20/08/0223/08/02

Keywords

  • FMT-MC: MODEL CHECKING
  • FMT-PM: PROBABILISTIC METHODS
  • IR-63323
  • FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
  • EWI-6522

Cite this

Brim, J. (Ed.), Baier, C., Katoen, J. P., Jancar, P. (Ed.), Hermanns, H., Kretnsk, M. (Ed.), ... Kucera, A. (Ed.) (2002). Simulation for continuous-time Markov chains. 473-489. Paper presented at 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic. https://doi.org/10.1007/3-540-45694-5_23
Brim, J. (Editor) ; Baier, Christel ; Katoen, Joost P. ; Jancar, P. (Editor) ; Hermanns, H. ; Kretnsk, M. (Editor) ; Haverkort, Boudewijn R.H.M. ; Kucera, A. (Editor). / Simulation for continuous-time Markov chains. Paper presented at 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic.15 p.
@conference{b29d0b55e3d9499592a269241d02a85e,
title = "Simulation for continuous-time Markov chains",
abstract = "This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.",
keywords = "FMT-MC: MODEL CHECKING, FMT-PM: PROBABILISTIC METHODS, IR-63323, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, EWI-6522",
author = "J. Brim and Christel Baier and Katoen, {Joost P.} and P. Jancar and H. Hermanns and M. Kretnsk and Haverkort, {Boudewijn R.H.M.} and A. Kucera",
year = "2002",
doi = "10.1007/3-540-45694-5_23",
language = "Undefined",
pages = "473--489",
note = "null ; Conference date: 20-08-2002 Through 23-08-2002",

}

Brim, J (ed.), Baier, C, Katoen, JP, Jancar, P (ed.), Hermanns, H, Kretnsk, M (ed.), Haverkort, BRHM & Kucera, A (ed.) 2002, 'Simulation for continuous-time Markov chains' Paper presented at 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic, 20/08/02 - 23/08/02, pp. 473-489. https://doi.org/10.1007/3-540-45694-5_23

Simulation for continuous-time Markov chains. / Brim, J. (Editor); Baier, Christel; Katoen, Joost P.; Jancar, P. (Editor); Hermanns, H.; Kretnsk, M. (Editor); Haverkort, Boudewijn R.H.M.; Kucera, A. (Editor).

2002. 473-489 Paper presented at 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic.

Research output: Contribution to conferencePaperAcademicpeer-review

TY - CONF

T1 - Simulation for continuous-time Markov chains

AU - Baier, Christel

AU - Katoen, Joost P.

AU - Hermanns, H.

AU - Haverkort, Boudewijn R.H.M.

A2 - Brim, J.

A2 - Jancar, P.

A2 - Kretnsk, M.

A2 - Kucera, A.

PY - 2002

Y1 - 2002

N2 - This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

AB - This paper presents a simulation preorder for continuous-time Markov chains (CTMCs). The simulation preorder is a conservative extension of a weak variant of probabilistic simulation on fully probabilistic systems, i.e., discrete-time Markov chains. The main result of the paper is that the simulation preorder preserves safety and liveness properties expressed in continuous stochastic logic (CSL), a stochastic branching-time temporal logic interpreted over CTMCs.

KW - FMT-MC: MODEL CHECKING

KW - FMT-PM: PROBABILISTIC METHODS

KW - IR-63323

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - EWI-6522

U2 - 10.1007/3-540-45694-5_23

DO - 10.1007/3-540-45694-5_23

M3 - Paper

SP - 473

EP - 489

ER -

Brim J, (ed.), Baier C, Katoen JP, Jancar P, (ed.), Hermanns H, Kretnsk M, (ed.) et al. Simulation for continuous-time Markov chains. 2002. Paper presented at 13th International Conference on Concurrency Theory, CONCUR 2002, Brno, Czech Republic. https://doi.org/10.1007/3-540-45694-5_23