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

DOI10.1016/J.TCS.2007.05.006MaRDI QIDQ995461zbMATH OpenOpenAlexFDO

Authors 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)

Recommendations

• scientific article; zbMATH DE number 1538068
• scientific article; zbMATH DE number 1670870
• Performability assessment by model checking of Markov reward models
• scientific article; zbMATH DE number 1946767
• scientific article; zbMATH DE number 1890701

Cites work

• scientific article; zbMATH DE number 1670870 (Why is no real title available?)
• scientific article; zbMATH DE number 3522951 (Why is no real title available?)
• scientific article; zbMATH DE number 1361121 (Why is no real title available?)
• scientific article; zbMATH DE number 729460 (Why is no real title available?)
• scientific article; zbMATH DE number 1946766 (Why is no real title available?)
• scientific article; zbMATH DE number 2087806 (Why is no real title available?)
• scientific article; zbMATH DE number 1884417 (Why is no real title available?)
• scientific article; zbMATH DE number 763717 (Why is no real title available?)
• scientific article; zbMATH DE number 3361677 (Why is no real title available?)
• Interactive Markov chains. And the quest for quantified quality
• Model checking expected time and expected reward formulae with random time bounds
• On the solution of GSPN reward models
• On the usability of process algebra: An architectural view
• Performance measure sensitive congruences for Markovian process algebras
• Reward model solution methods with impulse and rate rewards: an algorithm and numerical results
• Specification techniques for Markov reward models

Cited in

(2)

• Measuring with timed patterns
• Model checking for performability

Describes a project that uses

Uses Software

• PRISM
• SMART_
• MRMC
• PEPA

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q995461)