Abstract

This thesis introduces the model of Weighted Probabilistic Timed Automata (WPTA). WPTA are an extension of the well known Timed Automata. With WPTA we can make a specification of systems that have discrete control, and continuous real-time behaviour. Moreover we can model cost-per-time, depending on the discrete state, and we can model probability on the discrete behaviour. An example of a system that can be modeled as WPTA is a task-scheduling problem with cost-per-time on resources, and resources being available with a certain probability.

The question is whether model checking, i. e. the automatic verification of certain properties, is possible on WPTA. Our research focused on methods for deciding whether a certain discrete state is reachable from the stating state, with cost below a certain boundary, and a certain minimal probability. Our research resulted in three algorithms. We assume a given cost-bound. The first algorithm is a backward algorithm that uses priced zones. It solves the problem when we are only interested in a positive probability instead of the exact value. The second algorithm constructs an upper bound on the probability for which the property holds. The third algorithm possibly does not terminate, but it generates an ascending sequence of values that converges to the maximum probability. In this way if a state exists such that the property holds, then we can conclude this. But if such a state does not exist we cannot give a verdict.

Additional Resources

1. The paper