Model Checking Nondeterministic and Randomly Timed Systems

M. Neuhausser

    Research output: ThesisPhD Thesis - Research external, graduation UT

    110 Downloads (Pure)

    Abstract

    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
    Supervisors/Advisors
    • Katoen, Joost P., Supervisor
    Thesis sponsors
    Award date22 Jan 2010
    Place of PublicationZutphen, Netherlands
    Publisher
    Print ISBNs978-90-365-2975-4
    DOIs
    Publication statusPublished - 22 Jan 2010

      Fingerprint

    Keywords

    • EWI-18032
    • FMT-MC: MODEL CHECKING
    • IR-69565
    • METIS-270861

    Cite this

    Neuhausser, M. (2010). Model Checking Nondeterministic and Randomly Timed Systems. Zutphen, Netherlands: Wöhrmann Print Service. https://doi.org/10.3990/1.9789036529754