Model Checking pathCSL

Lucia Cloth; Boudewijn Haverkort; Holger Hermanns; Joost-Pieter Katoen; Christel Baier; Andrea Bobbio; Daniel Deavours; Yue Ma

Model Checking pathCSL

Lucia Cloth
, Boudewijn Haverkort
, Holger Hermanns
, Joost-Pieter Katoen
, Christel Baier
, Andrea Bobbio (Editor)
, Daniel Deavours (Editor)
, Yue Ma (Editor)

Research output: Other contribution

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 language	English
Publisher	University of Illinois at Urbana-Champaign
Number of pages	4
Place of Publication	Urbana-Champaign
Publication status	Published - 6 Sept 2003
Externally published	Yes

Keywords

METIS-216859

Cite this

@misc{f2164e568602429582019a1c88acd43b,

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 and Andrea Bobbio and Daniel Deavours and Yue Ma",

year = "2003",

month = sep,

day = "6",

language = "English",

publisher = "University of Illinois at Urbana-Champaign",

type = "Other",

}

TY - GEN

T1 - Model Checking pathCSL

AU - Cloth, Lucia

AU - Haverkort, Boudewijn

AU - Hermanns, Holger

AU - Katoen, Joost-Pieter

AU - Baier, Christel

A2 - Bobbio, Andrea

A2 - Deavours, Daniel

A2 - Ma, Yue

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 - Other contribution

PB - University of Illinois at Urbana-Champaign

CY - Urbana-Champaign

ER -

Model Checking pathCSL

Abstract

Keywords

Fingerprint

Cite this