Model Checking Structured Infinite Markov Chains

Anne Katharina Ingrid Remke

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    71 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 Remigius Heinrich Maria, 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, A. K. I. (2008). Model Checking Structured Infinite Markov Chains. Zutphen: Woermann Printing Service. https://doi.org/10.3990/1.9789085703044