Submitted: March 2013
Abstract
Probabilistic automata have seen various applications in the formal specification and verification of reactive and concurrent systems. Most model-checking tools, which support probabilistic system, for example PRISM, operate on state-labelled probabilistic automata, which express how properties of a system may evolve over time and thus, attach labels to states. On the other hand, transition-labelled probabilistic automata can express how a system behaves in terms of the actions it can perform. Here, transitions are labelled by actions whereas states remain unlabelled. Many behavioural equivalences like strong and weak bisimulation have been studied on transition-labelled probabilistic automata and can be efficiently decided. Clearly, both variations of probabilistic automata are important tools with different techniques and tools tailored towards them. This separation is not desirable as we want to apply techniques and tools for state-labelled probabilistic automata also to transition-labelled ones and vice versa.
Thus, this thesis aims to overcome this limitation in the spirit of de Nicola and Vaandrager, who solved this problem for Kripke structures and labelled transition systems, by defining translations from state-labelled probabilistic automata to transition-labelled probabilistic automata and vice versa. In addition, we introduce the logic APCTL*, an adaption of PCTL* for transition-labelled probabilistic automata and show that arbitrary logic formulae of one logic can be efficiently translated into a formulae of the other logic, while there truth value is fully preserved in the translated automaton.