MC=MC: Model Checking Infinite-State Markov Chains
J.-P. Katoen, I.S. Zapreev, B.R. Haverkort (U. Twente, NL), A. Remke (U. Twente, NL)
(funded by the NWO)
Model-based performance evaluation aims at forecasting system behaviour in a quantitative way, starting from an abstract system model. Due to the ever-increasing size and complexity of modern computer and communication systems, performance models that are directly amenable to a numerical solution are often generated from high-level modelling languages, based, e.g., on stochastic Petri nets or stochastic process algebras. For a significant class of systems, these models turn out to be infinite state, and need to be analysed by specific techniques, such as matrix-geometric methods.
Recently, extensions to temporal logics have been developed to ease the specification of important measures-of-interest (like reponse times, or the probability to reach deadlines) over performance models, and logic-based verification algorithms have been integrated with numerical means to automatically check these properties. This novel approach is, however, still restricted to finite-state systems.
This project aims to establish a cross-fertilization between (i) performance evaluation techniques for infinite-state systems and (ii) logic-based model-checking algorithms for Markov chains. The goal is to develop algorithms and a prototype software tool for the specification and automated evaluation of performance measures for infinite-state Markov chains, and to apply these to case studies with realistic complexity.
This project also takes place as part of the VOSS2 project.
J.-P. Katoen, I.S. Zapreev, B.R. Haverkort (U. Twente, NL), A. Remke (U. Twente, NL)
(funded by the NWO)
Model-based performance evaluation aims at forecasting system behaviour in a quantitative way, starting from an abstract system model. Due to the ever-increasing size and complexity of modern computer and communication systems, performance models that are directly amenable to a numerical solution are often generated from high-level modelling languages, based, e.g., on stochastic Petri nets or stochastic process algebras. For a significant class of systems, these models turn out to be infinite state, and need to be analysed by specific techniques, such as matrix-geometric methods.
Recently, extensions to temporal logics have been developed to ease the specification of important measures-of-interest (like reponse times, or the probability to reach deadlines) over performance models, and logic-based verification algorithms have been integrated with numerical means to automatically check these properties. This novel approach is, however, still restricted to finite-state systems.
This project aims to establish a cross-fertilization between (i) performance evaluation techniques for infinite-state systems and (ii) logic-based model-checking algorithms for Markov chains. The goal is to develop algorithms and a prototype software tool for the specification and automated evaluation of performance measures for infinite-state Markov chains, and to apply these to case studies with realistic complexity.
This project also takes place as part of the VOSS2 project.