Workshop on Process Algebra and Stochastically Timed Activities (PASTA)

Thursday 13th June 2002
Laboratory for Foundations of Computer Science
The University of Edinburgh
Edinburgh, UK

Programme

9:45	Welcome and opening remarks
10:00	Linda Brodo	A stochastic pi-calculus semantics for PEPA nets
10:30	Leïla Kloul	From SAN to PEPA: A technology transfer
11:00	Coffee break
11:30	Jeremy Bradley	Ants and agents
12:00	Stephen Gilmore	Software performance design environments
12:30	Lunch
2:00	Jane Hillston	Systematic transformations to find quasi-reversible structures in PEPA models
2:30	Nigel Thomas	Behavioural independence and control in PEPA
3:00	Richard Hopkins	Residual time transition systems (for STOCON Nets)
3:30	Coffee break
4:00	Mario Bravetti	An integrated approach for the specification and analysis of stochastic real-time systems
5:00	Close
8:00	Workshop dinner: The Marque restaurant, 19 - 21 Causewayside

Abstracts


Linda Brodo	Università degli Studi di Verona
	A stochastic pi-calculus semantics for PEPA nets
	We provide a semantics for a subset of the PEPA nets modelling language by mapping it into the stochastic pi-calculus. The mapping provides an opportunity to contrast the well-known small-step semantics style with the definition induced by language embedding and to study the definitions of equivalences between models in the two styles.

Leïla Kloul	University of Edinburgh
	From SAN to PEPA: A technology transfer
	In this talk, I will present the functional dependencies introduced in PEPA to capture the exact timing behaviour of cooperating PEPA activities. Through examples, I will show the advantages of using these dependencies in terms of flexibility in constructing the model and reduction of the model size. Moreover the use of functional dependencies allows us to have a direct tensorial representation of the Markov process underlying a PEPA model. I will finish by talking about the cost of performing the matrix-vector multiplications which may depend on the functional dependencies.

Jeremy Bradley	Imperial College, London
	Ants and Agents
	(Based on work by David Sumpter)
	We look at some recent work which shows how complex behaviour in biological systems, in this case colonies of ants, can be created from many interacting individuals running very simple process algebra programs. These systems represent the ultimate in massive parallelism without any central control (or server) and turn out to be very suitable for analysis using stochastic process algebras. We will also introduce a Mean Field Analysis technique used in David Sumpter's papers to extract mean transient behaviour from these large concurrent systems, and discuss how it might be applied to PEPA.

Stephen Gilmore	The University of Edinburgh
	Software performance design environments
	We describe a software toolset which allows UML modellers to annotate their models with performance information. An equivalent performance model is extracted from the UML, solved, and the results reflected back to the UML level. Used in this way, our toolset gives a high-level approach to software performance modelling where the benefits of the performance modelling process are achieved without significant additional notational burden.

Jane Hillston	The University of Edinburgh
	Systematic transformations to find quasi-reversible structures in PEPA models
	Efficient product form solution is one of the major attractions of queueing networks for performance modelling purposes. These models rely on a form of interaction between nodes in a network which allows them to be solved in isolation, since they behave as if independent up to normalisation. Several papers have explored the extent to which product form structures can be identified in models expressed in a Markovian process algebra (MPA). Previously Harrison and Hillston presented a syntactic characterisation of MPA models which give rise to quasi-reversible structure, leading to product form solution. This characterisation means that models may be systematically checked for the quasi-reversible property, without expanding the state space. It is one of the features of process algebra models, however, that different syntactic presentations may give rise to the same underlying structure. In this talk we describe a set of transformations which may be used to manipulate the syntactic presentation of a PEPA model, thus allowing a previously obscured quasi-reversible structure to be detected.

Nigel Thomas	University of Durham
	Behavioural independence and control in PEPA
	Models of complex systems are inherently difficult to solve due principally to the size of their underlying state space. In Markovian process algebra a significant amount of work has been done to tackle this problem by exploiting the compositional nature of models and identifying structures that are amenable to different approaches to decomposition. In this talk a slightly different approach is presented which concentrates on interaction between components and its impact on behaviour. Two notions are introduced, behavioural independence and control. Informally, behavioural independence exists when one group of components behaves in a way that is not directly influenced by the evolution of other components in the model. Conversely control exists when one or more components dictate the behaviour of another component by the occurrence of internal actions. In many cases these properties can be identified without exploring the underlying state space and their existence can be used to derive a number of different model decompositions and approximations. In particular well known approaches such as reversibility and quasi-separability are explored using this method to complement earlier results. A simple iterative approximation has also been applied to models exhibiting control to derive a numerical solution to marginal component distributions. The talk includes a number of worked examples to highlight the potential of this approach.

Richard Hopkins	Heriot-Watt University, Edinburgh
	Residual time transition systems
	STOCON (Stochastic Composable Nets) is formalism for concurrent systems, based on Petri nets enhanced with features for: (a) compositionality; (b) quantitative aspects of behaviour - probabilities and time delays. This talk focuses on representations of behaviour and qualitative analysis, for systems with arbitrarily distributed delays. The basic behaviour model is a labelled transition system (LTS). To obtain an adequate representation of behaviour in the presence of arbitrarily distributed delays requires some extensions to the basic LTS structure. Firstly, for delays not having the memoryless property, choice and parallel must be distinguished. This is achieved by associating explicit concurrency information with an LTS state, to give a Concurrency Transition System (CTS). Secondly, for qualitative analysis we require a representation of behaviour which: (a) makes explicit all qualitatively different behaviours; (b) (for automatability) is finite if the basic LTS is finite. The proposed representation is a Residual Time Transition System (RTTS) - a CTS enhanced with information about the remaining time to completion of transitions. This information is necessary to generate qualitative properties such as the set of traces. The RTTS provides an appropriate representation of behaviour for defining constructs such as qualitative observational equivalence.

Mario Bravetti	Università di Bologna
	An integrated approach for the specification and analysis of stochastic real-time systems
	A formal approach for the design and analysis of concurrent systems is proposed which integrates two different orthogonal aspects of time: (i) the aspect of probabilistic-time, concerning the probabilistic quantification of durations of system activities via (exponential) probability distributions and the evaluation of system performance, and (ii) the aspect of real-time, concerning the expression of time constraints and the verification of exact time properties. We show that these two aspects, that led to the introduction of different specification paradigms called Markovian process algebras and timed automata, respectively, can be expressed in an integrated way by a single language, namely a process algebra capable of expressing both probabilistic durations and time bounds via probability distributions of a general kind. We will present techniques for system analysis at the level of such an integrated specification as well as formal mappings for obtaining a pure (Markovian) probabilistic-time and a pure real-time system representation which are guaranteed to be consistent and can be analysed by using standard techniques and tools.