Model Checking Nondeterministic and Randomly Timed Systems

M. Neuhausser

Research output: ThesisPhD Thesis - Research external, graduation UTAcademic

63 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

Model checking
Packet networks

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
Neuhausser, M.. / Model Checking Nondeterministic and Randomly Timed Systems. Zutphen, Netherlands : Wöhrmann Print Service, 2010. 244 p.
@phdthesis{4824522f52d0466abd6911bb585d6b76,
title = "Model Checking Nondeterministic and Randomly Timed Systems",
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.",
keywords = "EWI-18032, FMT-MC: MODEL CHECKING, IR-69565, METIS-270861",
author = "M. Neuhausser",
note = "CTIT Ph.D.-Thesis Series No. 09-165, ISSN 1381-3617",
year = "2010",
month = "1",
day = "22",
doi = "10.3990/1.9789036529754",
language = "English",
isbn = "978-90-365-2975-4",
publisher = "W{\"o}hrmann Print Service",
address = "Netherlands",
school = "University of Twente",

}

Neuhausser, M 2010, 'Model Checking Nondeterministic and Randomly Timed Systems', University of Twente, Zutphen, Netherlands. https://doi.org/10.3990/1.9789036529754

Model Checking Nondeterministic and Randomly Timed Systems. / Neuhausser, M.

Zutphen, Netherlands : Wöhrmann Print Service, 2010. 244 p.

Research output: ThesisPhD Thesis - Research external, graduation UTAcademic

TY - THES

T1 - Model Checking Nondeterministic and Randomly Timed Systems

AU - Neuhausser, M.

N1 - CTIT Ph.D.-Thesis Series No. 09-165, ISSN 1381-3617

PY - 2010/1/22

Y1 - 2010/1/22

N2 - 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.

AB - 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.

KW - EWI-18032

KW - FMT-MC: MODEL CHECKING

KW - IR-69565

KW - METIS-270861

U2 - 10.3990/1.9789036529754

DO - 10.3990/1.9789036529754

M3 - PhD Thesis - Research external, graduation UT

SN - 978-90-365-2975-4

PB - Wöhrmann Print Service

CY - Zutphen, Netherlands

ER -

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