On the logical characterisation of performability properties

DOI10.1007/3-540-45022-X_65MaRDI QIDQ2754196zbMATH OpenFDO

Authors B. R. Haverkort, Holger Hermanns, Christel Baier, Joost-Pieter Katoen

Publication date 11 November 2001

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-45022-X_65

zbMATH Keywords

continuous stochastic logic

Mathematics Subject Classification ID

Performance evaluation, queueing, and scheduling in the context of computer systems (68M20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Performability assessment by model checking of Markov reward models
• Model checking for performability
• Automated performance and dependability evaluation using model checking
• Multiphase until formulas over Markov reward models: an algebraic approach
• Specification techniques for Markov reward models

Cited in

(19)

• On the use of MTBDDs for performability analysis and verification of stochastic systems.
• Model-checking large structured Markov chains.
• Computation tree measurement language (CTML)
• Performance measure sensitive congruences for Markovian process algebras
• Guarded autonomous transitions increase conciseness and expressiveness of timed automata
• Precisely deciding CSL formulas through approximate model checking for CTMCs
• Cost vs. time in stochastic games and Markov automata
• Model checking expected time and expected reward formulae with random time bounds
• Model checking for performability
• Model Checking Exact Cost for Attack Scenarios
• Exploiting modal logic to express performance measures
• Performance evaluation with temporal rewards
• Reward based congruences: Can we aggregate more?
• Action and State Based Computation Tree Measurement Language and Algorithms
• Component-oriented specification of performance measures
• Multiphase until formulas over Markov reward models: an algebraic approach
• Performability assessment by model checking of Markov reward models
• Mixing logics and rewards for the component-oriented specification of performance measures
• CSL model checking algorithms for QBDs

This page was built for publication: On the logical characterisation of performability properties

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