Extending the Logic IM-SPDL with Impulse and State Rewards


Haverkort, Boudewijn R. and Kuntz, Matthias (2007) Extending the Logic IM-SPDL with Impulse and State Rewards. [Report]

open access
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.
Item Type:Report
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/64330
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 241882