Symbolic Semantics and Verification of Stochastic Process Algebras

In the realm of performance and reliability analysis, high-level specification languages like stochastic process algebras (SPA) or generalised stochastic Petri nets (GSPN) have turned out to be extremely useful. During the analysis of systems, being specified with either of the two methods, two main problems can be identified: 1. State space explosion: This problem occurs on generation and storage of the semantic models of complex systems on which analysis is carried out. This semantic model is normally some kind of a continuous time Markov chain (CTMC) or stochastic labelled transition system (SLTS). 2. The specification and automatic verification of complex system requirements The state space explosion problem arises mainly in the context of the analysis of concur-rent systems. This is the type of systems, for which we want to devise analysis methods in this thesis. If the system is specified using SPAs, it is composed of many parallel processes. The overall state space of such a model is then the Cartesian product of the state spaces of the respective subprocesses. Thus, the memory requirements for storing the SLTSs of com-plex systems are often prohibitive. To combat this problem several steps must be taken. A