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

Matthias Kuntz, Boudewijn R. Haverkort, L. Cloth

Research output: Other contributionOther research output

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 languageEnglish
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages7
Place of PublicationEnschede
Publication statusPublished - Sep 2007
Externally publishedYes

Fingerprint

Stochastic models
Semantics
Model checking
Random processes
Petri nets
Algebra

Keywords

  • EWI-10988
  • METIS-241873
  • IR-64323

Cite this

Kuntz, M., Haverkort, B. R., & Cloth, L. (2007, Sep). GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. Enschede: Centre for Telematics and Information Technology (CTIT).
Kuntz, Matthias ; Haverkort, Boudewijn R. ; Cloth, L. / GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. 2007. Enschede : Centre for Telematics and Information Technology (CTIT). 7 p.
@misc{c1abf33cc170469088b9cb378c7d5945,
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.",
keywords = "EWI-10988, METIS-241873, IR-64323",
author = "Matthias Kuntz and Haverkort, {Boudewijn R.} and L. Cloth",
year = "2007",
month = "9",
language = "English",
publisher = "Centre for Telematics and Information Technology (CTIT)",
type = "Other",

}

Kuntz, M, Haverkort, BR & Cloth, L 2007, GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. Centre for Telematics and Information Technology (CTIT), Enschede.

GCSRL - A Logic for Stochastic Reward Models with Timed and Untimed Behaviour. / Kuntz, Matthias; Haverkort, Boudewijn R.; Cloth, L.

7 p. Enschede : Centre for Telematics and Information Technology (CTIT). 2007, .

Research output: Other contributionOther research output

TY - GEN

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

AU - Kuntz, Matthias

AU - Haverkort, Boudewijn R.

AU - Cloth, L.

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.

KW - EWI-10988

KW - METIS-241873

KW - IR-64323

M3 - Other contribution

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -