REACHABILITY ANAYSIS IN CONTINUOUSTIME MARKOV DECISION PROCESSES 


Reachability anaysis in continuoustime Markov decision processes Logics towards POMDP with and/or without rewards Energy consumption in AdHoc and Sensor Networks Stochastic Interfaces An eclipse environment for Modest (finished) Analysis of an Airbag Control Unit (finished) Title Reachability analysis in continuoustime Markov decision processes (finished) Content The ETMCC model checker is a Java based model checking tool for continuoustime Markov chains (CTMCs). Given a system that can be modelled as CTMC and a particular property P, formalized in a logic called continous stochastic logic (CSL), ETMCC aids in answering the question if the system satisfies P or not. Recently, this approach was improved at the University of Twente by reimplementing ETMCC in C++ using more efficient datastructures. The tool is called MRMC.
Meanwhile, we have extended ETMCC with a brandnew efficient algorithm for model checking continuoustime Markov decision processes which are an extension of CTMCs that incorporate nondeterminism. This implementation is used in the context of the European Train Control System (ETCS) to estimate, e.g., the probability that a particular train has to break within a given amount of time. Motivated by this, the goal of the thesis is to implement a C++ version of the above mentioned algorithm and to integrate it into the C++ implementation of MRMC. Prerequisites Programming skills in C++. Status Available. Contact References


Dependable Systems & Software Group  Department of Computer Science  Universität des Saarlandes 