Model-Checking of Infinite-State Markov Chains

Project Manager: Prof. dr. B.R.H.M. Haverkort

Faculty of Electrical Engineering, Mathematics and Computer Science - EEMCS

Tel.: +31-53-4893766

Project website:

Project Summary

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 for 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 proposal 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.

MC=MC publications UT

Project duration: 2003-2007

Number of person/years CTIT: 2.4 fte

Involved groups: Design and Analysis of Communication Systems (DACS), Formal Methods and Tools (FMT)

CTIT Strategic Research Orientation: DSN - Dependable Systems and Networks

	CTIT Home > ... > Open Competition > MC=MC
Home CTIT Symposium 2012 About CTIT News NIRICT Research Meet the PhDs Working at CTIT Internal Information Conferences Open Calls (updated April 20, 2012) Library and Videos Knowledge Transfer Links Sitemap Search	Model-Checking of Infinite-State Markov Chains Project Manager: Prof. dr. B.R.H.M. Haverkort Faculty of Electrical Engineering, Mathematics and Computer Science - EEMCS Tel.: +31-53-4893766 Email: boudewijn.haverkort@utwente.nl Project website: Project Summary 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 for 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 proposal 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. MC=MC publications UT Project duration: 2003-2007 Number of person/years CTIT: 2.4 fte Involved groups: Design and Analysis of Communication Systems (DACS), Formal Methods and Tools (FMT) CTIT Strategic Research Orientation: DSN - Dependable Systems and Networks