GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour

Matthias Kuntz; Boudewijn R. Haverkort

GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

60 Downloads (Pure)

Abstract

In this paper we define the logic GCSRL (generalised continuous stochastic reward logic) that provides means to reason about systems that have states which sojourn times are either greater zero, in which case this sojourn time is exponentially distributed (tangible states), or zero (vanishing states). In case of generalised stochastic Petri nets (GSPNs) and stochastic process algebras it turned out that these vanishing states can be very useful when it comes to define system behaviour. In the same way these states are useful for defining system properties using stochastic logics. We extend both the semantic model and the semantics of CSRL such that it allows to attach impulse rewards to transitions emanating from vanishing states. We show by means of a small example how model checking GCSRL formulae works.

Original language	English
Title of host publication	Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8)
Editors	L. Cloth
Place of Publication	Enschede
Publisher	Centre for Telematics and Information Technology (CTIT)
Pages	50-56
Number of pages	7
Publication status	Published - Sept 2007
Event	8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007 - Edinburgh, United Kingdom Duration: 20 Sept 2007 → 21 Sept 2007 Conference number: 8

Publication series

Name	CTIT Workshop Proceedings
Publisher	Centre for Telematics and Information Technology, University of Twente
ISSN (Print)	1574-0846
ISSN (Electronic)	0929-0672

Workshop

Workshop	8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007
Abbreviated title	PMCCS
Country/Territory	United Kingdom
City	Edinburgh
Period	20/09/07 → 21/09/07

Access to Document

ArticleFinal published version, 110 KB

Cite this

Kuntz, Matthias ; Haverkort, Boudewijn R. / GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8). editor / L. Cloth. Enschede : Centre for Telematics and Information Technology (CTIT), 2007. pp. 50-56 (CTIT Workshop Proceedings).

@inproceedings{ec17bda9475441e092e662eb56fca61c,

title = "GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour",

abstract = "In this paper we define the logic GCSRL (generalised continuous stochastic reward logic) that provides means to reason about systems that have states which sojourn times are either greater zero, in which case this sojourn time is exponentially distributed (tangible states), or zero (vanishing states). In case of generalised stochastic Petri nets (GSPNs) and stochastic process algebras it turned out that these vanishing states can be very useful when it comes to define system behaviour. In the same way these states are useful for defining system properties using stochastic logics. We extend both the semantic model and the semantics of CSRL such that it allows to attach impulse rewards to transitions emanating from vanishing states. We show by means of a small example how model checking GCSRL formulae works.",

author = "Matthias Kuntz and Haverkort, {Boudewijn R.}",

year = "2007",

month = sep,

language = "English",

series = "CTIT Workshop Proceedings",

publisher = "Centre for Telematics and Information Technology (CTIT)",

pages = "50--56",

editor = "L. Cloth",

booktitle = "Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8)",

address = "Netherlands",

note = "8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007, PMCCS ; Conference date: 20-09-2007 Through 21-09-2007",

}

Kuntz, M & Haverkort, BR 2007, GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. in L Cloth (ed.), Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8). CTIT Workshop Proceedings, Centre for Telematics and Information Technology (CTIT), Enschede, pp. 50-56, 8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007, Edinburgh, United Kingdom, 20/09/07.

GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. / Kuntz, Matthias; Haverkort, Boudewijn R.
Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8). ed. / L. Cloth. Enschede: Centre for Telematics and Information Technology (CTIT), 2007. p. 50-56 (CTIT Workshop Proceedings).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour

AU - Kuntz, Matthias

AU - Haverkort, Boudewijn R.

N1 - Conference code: 8

PY - 2007/9

Y1 - 2007/9

N2 - In this paper we define the logic GCSRL (generalised continuous stochastic reward logic) that provides means to reason about systems that have states which sojourn times are either greater zero, in which case this sojourn time is exponentially distributed (tangible states), or zero (vanishing states). In case of generalised stochastic Petri nets (GSPNs) and stochastic process algebras it turned out that these vanishing states can be very useful when it comes to define system behaviour. In the same way these states are useful for defining system properties using stochastic logics. We extend both the semantic model and the semantics of CSRL such that it allows to attach impulse rewards to transitions emanating from vanishing states. We show by means of a small example how model checking GCSRL formulae works.

AB - In this paper we define the logic GCSRL (generalised continuous stochastic reward logic) that provides means to reason about systems that have states which sojourn times are either greater zero, in which case this sojourn time is exponentially distributed (tangible states), or zero (vanishing states). In case of generalised stochastic Petri nets (GSPNs) and stochastic process algebras it turned out that these vanishing states can be very useful when it comes to define system behaviour. In the same way these states are useful for defining system properties using stochastic logics. We extend both the semantic model and the semantics of CSRL such that it allows to attach impulse rewards to transitions emanating from vanishing states. We show by means of a small example how model checking GCSRL formulae works.

M3 - Conference contribution

T3 - CTIT Workshop Proceedings

SP - 50

EP - 56

BT - Proceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8)

A2 - Cloth, L.

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

T2 - 8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007

Y2 - 20 September 2007 through 21 September 2007

ER -