Model Checking Nondeterministic and Randomly Timed Systems

M. Neuhausser

    Research output: ThesisPhD Thesis - Research external, graduation UT

    296 Downloads (Pure)


    Quantitative model checking has become an indispensable tool to analyze performance and dependability characteristics such as the expected round trip time in a packet switched network or the failure probability of a safety-critical system. So far, the existing model checking techniques lack support for models which combine stochastic timing and nondeterminism. This is surprising, as nondeterminism is the key for compositional modeling and occurs naturally in distributed systems. In this thesis, we overcome this limitation. More precisely, we consider continuous-time Markov decision processes (CTMDPs), a model which closely entangles stochasticity and nondeterminism. Our main contribution is a discretization which allows to compute the maximum and minimum probability to enter a set of goal states in a CTMDP within a given time-bound. By applying value iteration techniques to the induced discrete-time model, we compute the desired probabilities up to an a priori specified precision. This result provides the basis for model checking important performance and dependability characteristics and has been extended to a variety of other nondeterministic and randomly timed system models. We demonstrate the applicability of our techniques by a number of case studies which also show that nondeterministic modeling makes an essential difference in the area of performance and dependability evaluation.
    Original languageEnglish
    Awarding Institution
    • University of Twente
    • Katoen, Joost-Pieter, Supervisor
    Thesis sponsors
    Award date22 Jan 2010
    Place of PublicationZutphen, Netherlands
    Print ISBNs978-90-365-2975-4
    Publication statusPublished - 22 Jan 2010


    • EWI-18032
    • IR-69565
    • METIS-270861


    Dive into the research topics of 'Model Checking Nondeterministic and Randomly Timed Systems'. Together they form a unique fingerprint.

    Cite this