Algebras and Automata for Timed and Stochastic Systems
| Title | Algebras and Automata for Timed and Stochastic Systems |
| Publication Type | Thesis |
| Year of Publication | 1999 |
| Authors | D'Argenio, PR |
| Academic Department | Department of Computer Science, University of Twente |
| Degree | PhD in Computer Science |
| University | Department of Computer Science, University of Twente |
| City | Enschede |
| Thesis Type | phd |
| ISBN Number | 90-365-1363-4 |
| Abstract | In this thesis we introduce and study process algebras and automata for the design and analysis of timed and stochastic systems. In the first part we introduce a process algebra for timed systems which we call (read hearts). provides a language that allows a modular and hierarchical modelling of timed systems. Its rigorously defined semantics is given in terms of timed automata, a well-established model for the analysis of timed systems. We provide an axiomatisation for . The interest of having an axiom system is two-fold. First, the concept of algebra is fundamental in mathematics. Therefore, an axiomatisation will help on the understanding of the process algebra and the concepts it involves. Second, the analysis and verification of systems described using can be partially or completely carried out by means of equational reasoning. In the second part of the thesis, a theory for the description and analysis of stochastic systems is defined. We first introduce probabilistic transition systems which allow arbitrary probability distributions. As a consequence, stochastically distributed dense time can be represented in a straightforward manner. A probabilistic bisimulation is defined on this model. The use of probabilistic transition systems as a specification model is not attractive however since they are highly infinite objects. Therefore, we define a new model based on generalised semi-Markov processes and timed automata which we call stochastic automata. The stochastic automata model is a general symbolic stochastic model that provides an adequate framework for composition. Its semantics is given in terms of probabilistic transition systems. Using stochastic automata as the underlying semantic model, we define (read spades), a process algebra for stochastic automata. This stochastic process algebra considers arbitrary distributions and non-determinism. A particular characteristic is that parallel composition and synchronisation can be easily defined in the model, and it can be algebraically decomposed in terms of more primitive operations according to a so-called expansion law. In order to show the feasibility of the analysis of systems specified in we report on algorithms and prototypical tools we have developed to study correctness as well as performance and reliability. The tools were used to analyse several case studies that are reported as well. |
| URL | dissertation |
PDF (Full text):
