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

Matthias Kuntz, Boudewijn R. Haverkort

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    25 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 languageEnglish
    Title of host publicationProceedings of the Eighth International Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-8)
    EditorsL. Cloth
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Pages50-56
    Number of pages7
    Publication statusPublished - Sep 2007
    Event8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007 - Edinburgh, United Kingdom
    Duration: 20 Sep 200721 Sep 2007
    Conference number: 8

    Publication series

    NameCTIT Workshop Proceedings
    PublisherCentre for Telematics and Information Technology, University of Twente
    ISSN (Print)1574-0846
    ISSN (Electronic)0929-0672

    Workshop

    Workshop8th International Workshop on Performability Modeling of Computer and Communication Systems, PMCCS 2007
    Abbreviated titlePMCCS
    CountryUnited Kingdom
    CityEdinburgh
    Period20/09/0721/09/07

      Fingerprint

    Keywords

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

    Cite this

    Kuntz, M., & Haverkort, B. R. (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) (pp. 50-56). (CTIT Workshop Proceedings). Enschede: Centre for Telematics and Information Technology (CTIT).