Extending the Logic IM-SPDL with Impulse and State Rewards

Research output: Book/ReportBookScientific

Abstract

This report presents the logic SDRL (Stochastic Dynamic Reward Logic), an extension of the stochastic logic IM-SPDL, which supports the specication of complex performance and dependability requirements. SDRL extends IM-SPDL with the possibility to express impulse- and state reward measures. The logic is interpreted over extended action-based Markov reward model (EMRM), i.e. transition systems containing both immediate and Markovian transitions, where additionally the states and transitions can be enriched with rewards. We define ne the syntax and semantics of the new logic and show that SDRL provides powerful means to specify path-based properties with timing and reward-based restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of SDRL time- and reward-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the EMRM is built and subsequently transformed into a continuous time Markov reward model (MRM) on which numerical analysis is performed.
Original languageEnglish
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Publication statusPublished - Sep 2007
Externally publishedYes

Publication series

NameCTIT Technical Report Series

Fingerprint

Model checking
Numerical analysis
Semantics

Keywords

  • METIS-241882
  • EWI-11006
  • IR-64330

Cite this

Kuntz, G. W. M., & Haverkort, B. R. H. M. (2007). Extending the Logic IM-SPDL with Impulse and State Rewards. (CTIT Technical Report Series). Enschede: Centre for Telematics and Information Technology (CTIT).
Kuntz, G.W.M. ; Haverkort, Boudewijn R.H.M. / Extending the Logic IM-SPDL with Impulse and State Rewards. Enschede : Centre for Telematics and Information Technology (CTIT), 2007. (CTIT Technical Report Series).
@book{75a01683587f46fa98e7eea55a71eb56,
title = "Extending the Logic IM-SPDL with Impulse and State Rewards",
abstract = "This report presents the logic SDRL (Stochastic Dynamic Reward Logic), an extension of the stochastic logic IM-SPDL, which supports the specication of complex performance and dependability requirements. SDRL extends IM-SPDL with the possibility to express impulse- and state reward measures. The logic is interpreted over extended action-based Markov reward model (EMRM), i.e. transition systems containing both immediate and Markovian transitions, where additionally the states and transitions can be enriched with rewards. We define ne the syntax and semantics of the new logic and show that SDRL provides powerful means to specify path-based properties with timing and reward-based restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of SDRL time- and reward-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the EMRM is built and subsequently transformed into a continuous time Markov reward model (MRM) on which numerical analysis is performed.",
keywords = "METIS-241882, EWI-11006, IR-64330",
author = "G.W.M. Kuntz and Haverkort, {Boudewijn R.H.M.}",
year = "2007",
month = "9",
language = "English",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",

}

Kuntz, GWM & Haverkort, BRHM 2007, Extending the Logic IM-SPDL with Impulse and State Rewards. CTIT Technical Report Series, Centre for Telematics and Information Technology (CTIT), Enschede.

Extending the Logic IM-SPDL with Impulse and State Rewards. / Kuntz, G.W.M.; Haverkort, Boudewijn R.H.M.

Enschede : Centre for Telematics and Information Technology (CTIT), 2007. (CTIT Technical Report Series).

Research output: Book/ReportBookScientific

TY - BOOK

T1 - Extending the Logic IM-SPDL with Impulse and State Rewards

AU - Kuntz, G.W.M.

AU - Haverkort, Boudewijn R.H.M.

PY - 2007/9

Y1 - 2007/9

N2 - This report presents the logic SDRL (Stochastic Dynamic Reward Logic), an extension of the stochastic logic IM-SPDL, which supports the specication of complex performance and dependability requirements. SDRL extends IM-SPDL with the possibility to express impulse- and state reward measures. The logic is interpreted over extended action-based Markov reward model (EMRM), i.e. transition systems containing both immediate and Markovian transitions, where additionally the states and transitions can be enriched with rewards. We define ne the syntax and semantics of the new logic and show that SDRL provides powerful means to specify path-based properties with timing and reward-based restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of SDRL time- and reward-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the EMRM is built and subsequently transformed into a continuous time Markov reward model (MRM) on which numerical analysis is performed.

AB - This report presents the logic SDRL (Stochastic Dynamic Reward Logic), an extension of the stochastic logic IM-SPDL, which supports the specication of complex performance and dependability requirements. SDRL extends IM-SPDL with the possibility to express impulse- and state reward measures. The logic is interpreted over extended action-based Markov reward model (EMRM), i.e. transition systems containing both immediate and Markovian transitions, where additionally the states and transitions can be enriched with rewards. We define ne the syntax and semantics of the new logic and show that SDRL provides powerful means to specify path-based properties with timing and reward-based restrictions. In general, paths can be characterised by regular expressions, also called programs, where the executability of a program may depend on the validity of test formulae. For the model checking of SDRL time- and reward-bounded path formulae, a deterministic program automaton is constructed from the requirement. Afterwards the product transition system between this automaton and the EMRM is built and subsequently transformed into a continuous time Markov reward model (MRM) on which numerical analysis is performed.

KW - METIS-241882

KW - EWI-11006

KW - IR-64330

M3 - Book

T3 - CTIT Technical Report Series

BT - Extending the Logic IM-SPDL with Impulse and State Rewards

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Kuntz GWM, Haverkort BRHM. Extending the Logic IM-SPDL with Impulse and State Rewards. Enschede: Centre for Telematics and Information Technology (CTIT), 2007. (CTIT Technical Report Series).