Model Checking pathCSL

Lucia Cloth, Boudewijn Haverkort, Holger Hermanns, Joost-Pieter Katoen, Christel Baier

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

4 Downloads (Pure)

Abstract

CSL formulas and path-based reward variables are two ways of specifying performability measures which depend on a sequence of states in a CTMC. We present the new logic pathCSL which combines ideas and advantages of both approaches.
Original languageEnglish
Title of host publicationPMCCS-6
Subtitle of host publicationThe Sixth International Workshop on Performability Modeling of Computer and Communication Systems
EditorsAndrea Bobbio, Daniel Deavours, Yue Ma
Place of PublicationUrbana-Champaign
PublisherUniversity of Illinois at Urbana-Champaign
Pages19-22
Publication statusPublished - 6 Sep 2003
Event6th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2003 - Monticello, United States
Duration: 6 Sep 20037 Sep 2003
Conference number: 6

Conference

Conference6th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2003
Abbreviated titlePMCCS
CountryUnited States
CityMonticello
Period6/09/037/09/03

Fingerprint

Performability
Reward
Model Checking
Logic
Path

Keywords

  • METIS-216859

Cite this

Cloth, L., Haverkort, B., Hermanns, H., Katoen, J-P., & Baier, C. (2003). Model Checking pathCSL. In A. Bobbio, D. Deavours, & Y. Ma (Eds.), PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems (pp. 19-22). Urbana-Champaign: University of Illinois at Urbana-Champaign.
Cloth, Lucia ; Haverkort, Boudewijn ; Hermanns, Holger ; Katoen, Joost-Pieter ; Baier, Christel. / Model Checking pathCSL. PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems. editor / Andrea Bobbio ; Daniel Deavours ; Yue Ma. Urbana-Champaign : University of Illinois at Urbana-Champaign, 2003. pp. 19-22
@inproceedings{68e8c6354121481f82edb201f9df3643,
title = "Model Checking pathCSL",
abstract = "CSL formulas and path-based reward variables are two ways of specifying performability measures which depend on a sequence of states in a CTMC. We present the new logic pathCSL which combines ideas and advantages of both approaches.",
keywords = "METIS-216859",
author = "Lucia Cloth and Boudewijn Haverkort and Holger Hermanns and Joost-Pieter Katoen and Christel Baier",
year = "2003",
month = "9",
day = "6",
language = "English",
pages = "19--22",
editor = "Andrea Bobbio and Daniel Deavours and Yue Ma",
booktitle = "PMCCS-6",
publisher = "University of Illinois at Urbana-Champaign",
address = "United States",

}

Cloth, L, Haverkort, B, Hermanns, H, Katoen, J-P & Baier, C 2003, Model Checking pathCSL. in A Bobbio, D Deavours & Y Ma (eds), PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems. University of Illinois at Urbana-Champaign, Urbana-Champaign, pp. 19-22, 6th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2003, Monticello, United States, 6/09/03.

Model Checking pathCSL. / Cloth, Lucia; Haverkort, Boudewijn; Hermanns, Holger; Katoen, Joost-Pieter; Baier, Christel.

PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems. ed. / Andrea Bobbio; Daniel Deavours; Yue Ma. Urbana-Champaign : University of Illinois at Urbana-Champaign, 2003. p. 19-22.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

TY - GEN

T1 - Model Checking pathCSL

AU - Cloth, Lucia

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

AU - Baier, Christel

PY - 2003/9/6

Y1 - 2003/9/6

N2 - CSL formulas and path-based reward variables are two ways of specifying performability measures which depend on a sequence of states in a CTMC. We present the new logic pathCSL which combines ideas and advantages of both approaches.

AB - CSL formulas and path-based reward variables are two ways of specifying performability measures which depend on a sequence of states in a CTMC. We present the new logic pathCSL which combines ideas and advantages of both approaches.

KW - METIS-216859

M3 - Conference contribution

SP - 19

EP - 22

BT - PMCCS-6

A2 - Bobbio, Andrea

A2 - Deavours, Daniel

A2 - Ma, Yue

PB - University of Illinois at Urbana-Champaign

CY - Urbana-Champaign

ER -

Cloth L, Haverkort B, Hermanns H, Katoen J-P, Baier C. Model Checking pathCSL. In Bobbio A, Deavours D, Ma Y, editors, PMCCS-6: The Sixth International Workshop on Performability Modeling of Computer and Communication Systems. Urbana-Champaign: University of Illinois at Urbana-Champaign. 2003. p. 19-22