Model Checking Structured Infinite Markov Chains

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

49 Downloads (Pure)

Abstract

In the past probabilistic model checking hast mostly been restricted to finite state models. This thesis explores the possibilities of model checking with continuous stochastic logic (CSL) on infinite-state Markov chains. We present an in-depth treatment of model checking algorithms for two special classes of infinite-state CTMCs: (i) Quasi-birth-death processes (QBDs) are a special class of infinite-state CTMCs that combines a large degree of modeling expressiveness with efficient solution methods. (ii) Jackson queuing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the CTMC that underlies a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues, whereas the underlying state-space of a QBD can be seen as infinite in one dimension. Using a new property-driven independency concept that is adapted to QBDs and JQNs, accordingly, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic termination criterion, the algorithms stop whenever the property to be checked can be certified (or falsified). Next to the above methodological contributions of this thesis, we also use the new techniques for an extended case study on bottlenecks in wireless two-hop ad hoc networks. The results of our analysis are compared with extensive simulations and show excellent agreement for throughput, mean number of active sources and mean buffer occupancy at the bottleneck station.
Original languageUndefined
Awarding Institution
  • University of Twente
Supervisors/Advisors
  • Haverkort, Boudewijn R.H.M., Supervisor
Thesis sponsors
Award date20 Jun 2008
Place of PublicationZutphen
Publisher
Print ISBNs978-90-8570-304-4
DOIs
Publication statusPublished - 20 Jun 2008

Keywords

  • IR-59013
  • METIS-251030
  • EWI-12927

Cite this

Remke, Anne Katharina Ingrid. / Model Checking Structured Infinite Markov Chains. Zutphen : Woermann Printing Service, 2008. 154 p.
@phdthesis{d2b4e0781d52422a93ebe7cce42ca2bb,
title = "Model Checking Structured Infinite Markov Chains",
abstract = "In the past probabilistic model checking hast mostly been restricted to finite state models. This thesis explores the possibilities of model checking with continuous stochastic logic (CSL) on infinite-state Markov chains. We present an in-depth treatment of model checking algorithms for two special classes of infinite-state CTMCs: (i) Quasi-birth-death processes (QBDs) are a special class of infinite-state CTMCs that combines a large degree of modeling expressiveness with efficient solution methods. (ii) Jackson queuing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the CTMC that underlies a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues, whereas the underlying state-space of a QBD can be seen as infinite in one dimension. Using a new property-driven independency concept that is adapted to QBDs and JQNs, accordingly, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic termination criterion, the algorithms stop whenever the property to be checked can be certified (or falsified). Next to the above methodological contributions of this thesis, we also use the new techniques for an extended case study on bottlenecks in wireless two-hop ad hoc networks. The results of our analysis are compared with extensive simulations and show excellent agreement for throughput, mean number of active sources and mean buffer occupancy at the bottleneck station.",
keywords = "IR-59013, METIS-251030, EWI-12927",
author = "Remke, {Anne Katharina Ingrid}",
note = "10.3990/1.9789085703044",
year = "2008",
month = "6",
day = "20",
doi = "10.3990/1.9789085703044",
language = "Undefined",
isbn = "978-90-8570-304-4",
publisher = "Woermann Printing Service",
school = "University of Twente",

}

Model Checking Structured Infinite Markov Chains. / Remke, Anne Katharina Ingrid.

Zutphen : Woermann Printing Service, 2008. 154 p.

Research output: ThesisPhD Thesis - Research UT, graduation UTAcademic

TY - THES

T1 - Model Checking Structured Infinite Markov Chains

AU - Remke, Anne Katharina Ingrid

N1 - 10.3990/1.9789085703044

PY - 2008/6/20

Y1 - 2008/6/20

N2 - In the past probabilistic model checking hast mostly been restricted to finite state models. This thesis explores the possibilities of model checking with continuous stochastic logic (CSL) on infinite-state Markov chains. We present an in-depth treatment of model checking algorithms for two special classes of infinite-state CTMCs: (i) Quasi-birth-death processes (QBDs) are a special class of infinite-state CTMCs that combines a large degree of modeling expressiveness with efficient solution methods. (ii) Jackson queuing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the CTMC that underlies a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues, whereas the underlying state-space of a QBD can be seen as infinite in one dimension. Using a new property-driven independency concept that is adapted to QBDs and JQNs, accordingly, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic termination criterion, the algorithms stop whenever the property to be checked can be certified (or falsified). Next to the above methodological contributions of this thesis, we also use the new techniques for an extended case study on bottlenecks in wireless two-hop ad hoc networks. The results of our analysis are compared with extensive simulations and show excellent agreement for throughput, mean number of active sources and mean buffer occupancy at the bottleneck station.

AB - In the past probabilistic model checking hast mostly been restricted to finite state models. This thesis explores the possibilities of model checking with continuous stochastic logic (CSL) on infinite-state Markov chains. We present an in-depth treatment of model checking algorithms for two special classes of infinite-state CTMCs: (i) Quasi-birth-death processes (QBDs) are a special class of infinite-state CTMCs that combines a large degree of modeling expressiveness with efficient solution methods. (ii) Jackson queuing networks (JQNs) are a very general class of queueing networks that find their application in a variety of settings. The state space of the CTMC that underlies a JQN, is highly structured, however, of infinite size in as many dimensions as there are queues, whereas the underlying state-space of a QBD can be seen as infinite in one dimension. Using a new property-driven independency concept that is adapted to QBDs and JQNs, accordingly, we provide model checking algorithms for all the CSL operators. Special emphasis is given to the time-bounded until operator for which we present a new and efficient computational procedure named uniformization with representatives. By the use of an application-driven dynamic termination criterion, the algorithms stop whenever the property to be checked can be certified (or falsified). Next to the above methodological contributions of this thesis, we also use the new techniques for an extended case study on bottlenecks in wireless two-hop ad hoc networks. The results of our analysis are compared with extensive simulations and show excellent agreement for throughput, mean number of active sources and mean buffer occupancy at the bottleneck station.

KW - IR-59013

KW - METIS-251030

KW - EWI-12927

U2 - 10.3990/1.9789085703044

DO - 10.3990/1.9789085703044

M3 - PhD Thesis - Research UT, graduation UT

SN - 978-90-8570-304-4

PB - Woermann Printing Service

CY - Zutphen

ER -