Chemnitz, Techn. Univ., Masterarb., 2008.

Zugl.: Saarbrücken, Univ., Diss., 2007

By combining two of the central paradigms of causality, namely counterfactual reasoning and probability-raising,we introduce a probabilistic notion of cause in Markov chains. Such a cause consists of finite executions of the probabilistic system after which the probability of an ω-regular effect exceeds a given threshold. The cause, as a set of executions, then has to cover all behaviors exhibiting the effect. With these properties, such causes can be used for monitoring purposes where the aim is to detect faulty behavior before it actually occurs. In order to choose which cause should be computed, we introduce multiple types of costs to capture the consumption of resources by the system or monitor from different perspectives, and study the complexity of computing cost-minimal causes.

Time-delayed actions appear as an essential component of numerous systems especially in evolution processes, natural phenomena, and particular technical applications and are associated with the existence of a memory. Under common conditions, external forces or state dependent parameters modify the length of the delay with time. Consequently, an altered dynamical behavior emerges, whose characterization is compulsory for a deeper understanding of these processes. In this thesis, the well-investigated class of time-homogeneous finite-state Markov processes is utilized to establish a variation of memory length by combining a first-order Markov chain with a memoryless Markov chain of order zero. The fluctuations induce a non-stationary process, which is accomplished for two special cases: a periodic and a random selection of the available Markov chains. For both cases, the Kolmogorov-Sinai entropy as a characteristic property is deduced analytically and compared to numerical approximations to the entropy rate of related symbolic dynamics. The convergences of per-symbol and conditional entropies are examined in order to recognize their behavior when identifying unknown processes. Additionally, the connection from Markov processes with varying memory length to hidden Markov models is illustrated enabling further analysis. Hence, the Kolmogorov-Sinai entropy of hidden Markov chains is calculated by means of Blackwell’s entropy rate involving Blackwell’s measure. These results are used to verify the previous computations.

Reliability of low-level operating-system (OS) code is an indispensable requirement. This includes functional properties from the safety-liveness spectrum, but also quantitative properties stating, e.g., that the average waiting time on locks is sufficiently small or that the energy requirement of a certain system call is below a given threshold with a high probability. This paper reports on our experiences made in a running project where the goal is to apply probabilistic model checking techniques and to align the results of the model checker with measurements to predict quantitative properties of low-level OS code.

Time-delayed actions appear as an essential component of numerous systems especially in evolution processes, natural phenomena, and particular technical applications and are associated with the existence of a memory. Under common conditions, external forces or state dependent parameters modify the length of the delay with time. Consequently, an altered dynamical behavior emerges, whose characterization is compulsory for a deeper understanding of these processes. In this thesis, the well-investigated class of time-homogeneous finite-state Markov processes is utilized to establish a variation of memory length by combining a first-order Markov chain with a memoryless Markov chain of order zero. The fluctuations induce a non-stationary process, which is accomplished for two special cases: a periodic and a random selection of the available Markov chains. For both cases, the Kolmogorov-Sinai entropy as a characteristic property is deduced analytically and compared to numerical approximations to the entropy rate of related symbolic dynamics. The convergences of per-symbol and conditional entropies are examined in order to recognize their behavior when identifying unknown processes. Additionally, the connection from Markov processes with varying memory length to hidden Markov models is illustrated enabling further analysis. Hence, the Kolmogorov-Sinai entropy of hidden Markov chains is calculated by means of Blackwell’s entropy rate involving Blackwell’s measure. These results are used to verify the previous computations.

Reliability of low-level operating-system (OS) code is an indispensable requirement. This includes functional properties from the safety-liveness spectrum, but also quantitative properties stating, e.g., that the average waiting time on locks is sufficiently small or that the energy requirement of a certain system call is below a given threshold with a high probability. This paper reports on our experiences made in a running project where the goal is to apply probabilistic model checking techniques and to align the results of the model checker with measurements to predict quantitative properties of low-level OS code.