Mixing logics and rewards for the component-oriented specification of performance measures

DOI10.1016/j.tcs.2007.05.006zbMath1159.68020OpenAlexW2170543783MaRDI QIDQ995461

Alessandro Aldini, Marco Bernardo

Publication date: 3 September 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2007.05.006

zbMATH Keywords

continuous-time Markov chainsstochastic process algebracomponent oriented modelingmeasure specification languagereward structures

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (1)

Model checking for performability

Uses Software

• PRISM
• SMART_
• MRMC
• PEPA

Cites Work

• Specification techniques for Markov reward models
• Interactive Markov chains. And the quest for quantified quality
• On the usability of process algebra: An architectural view
• Performance measure sensitive congruences for Markovian process algebras
• Model checking expected time and expected reward formulae with random time bounds
• On the solution of GSPN reward models
• Reward model solution methods with impulse and rate rewards: an algorithm and numerical results
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Mixing logics and rewards for the component-oriented specification of performance measures