MLQA 2012
From ERCIM Working Group MLQA
Joint Workshop on Compositional Modelling and Analysis of Quantitative SystemsSeptember 8, 2012 University of Edinburgh 

Contents 
Overview
The workshop combines the Fourth annual meeting of the ERCIM Working Group on Models and Logics for Quantitative Analysis (MLQA) with a SICSA Modelling and Abstraction Theme event.
The theme of the workshop is Compositional Modelling and Analysis of Quantitative Systems. Compositionality is a key concept in both the modeling and analysis of computer systems. It is only by decomposing large complex system into smaller pieces, we can build and analyse these systems.
The aim of the workshop is to bring together researchers working on quantitative modelling and analysis of computer systems focusing on research using compositional techniques. The workshop hopes to encourage interaction and collaboration between the attendees in developing compositional approaches. The workshop will bring together MLQA participants from across Europe with contributors to the SICSA theme of 'Modelling and Abstraction'. However, participation from outside MLQA and the SICSA theme are also welcome.
The workshop will take place immediately following the CONCUR International Conference taking place in NewcastleuponTyne 47th September 2012.
Invited speakers
 Pedro D'Argenio, FaMAF, Universidad Nacional de Cordoba
Security analysis in probabilistic distributed protocols via bounded reachability  Andrea Marin, Universita di Venezia
Compositional model specifications and analyses via productforms  Jaco van de Pol, University of Twente
Symbolic manipulation of markov automata  Mirco Tribastone, LudwigMaximiliansUniversität München
Exact aggregation for fluid process algebra models
Abstracts of the invited talks are available here.
Registration
Registration will be at a cost of £25. Registration is free for members of SICSA institutions.
Registration is available through the online registration system.
Posters
We invited posters under two categories:
 Presentation of recent or ongoing work in relation to the themes of MLQA.
 Overview of the recent research activities of a research group related to the themes of MLQA.
We equally encourage submissions from both research leaders, junior researchers and PhD students.
Posters should be printed by the participants in their preferred size.
Notification of your intention to submit, along with a title and short description of the poster, should be sent by August 31 to gethin.norman@glasgow.ac.uk.
Preliminary Programme
 09:30  09:45 Opening
 09:45  10:30 invited talk
 10:30  11:00 coffee
 11:00  11:45 Invited talk
 11:45  12:30 Invited talk
 12:30  14:00 lunch & poster session
 14:00  14:30 SICSA Contributed talk
 14:30  15:00 SICSA Contributed talk
 15:00  15:30 SICSA Contributed talk
 15:30  16:00 coffee
 16:00  17:00 MLQA business meeting
Travel and Accommodation
The workshop will take place at the Informatics Forum of the School of Informatics, University of Edinburgh. For details on its location as well as links for travel directions see here. For those attending CONCUR, Edinburgh is approximately 90 minutes from Newcastle by train.
For information regarding accommodation will be available soon.
Organisers
 Jane Hilston, University of Edinburgh
 Gethin Norman, University of Glasgow
Abstracts of Invited Talks
 Pedro D'Argenio, FaMAF, Universidad Nacional de Cordoba
Title: Security analysis in probabilistic distributed protocols via bounded reachability.
Abstract: Probabilistic model checking computes the probability values of a given property quantifying over all possible schedulers (also known as adversaries or policies). It turns out that maximum and minimum probabilities calculated in such a way are overestimations on models of distributed systems in which components are loosely coupled and share little information with each other. The problem exacerbates, if n addition the system is intended to protect private information.
In this talk, we will (1) discuss the problem, (2) give a characterization for the set of schedulers that respect the distributed nature of process and the idea of secrecy, (3) report of some important properties of this class of schedulers, and (4) present an algorithm to analyze timebounded reachability properties based on polynomial optimization. We will briefly discuss a prototype implementation and report some case studies.  Andrea Marin, Universita di Venezia
Title: Compositional model specifications and analyses via productforms
Abstract: Compositionality is an important aspect of many formalisms used for quantitative analysis of computer software and hardware architectures and communication systems. Compositionality allows for the specification of complex models in terms of cooperations of simpler components in a modular and hierarchical way.
However, these elegant and often compact model definitions often hide a huge complexity in the structure of the state space. For models with underlying continuous or discrete time Markov chains this implies that the quantitative evaluation of performance and reliability indices cannot rely on brute force approaches (such as the solution of the set of global balance equations). Therefore, from the point of view of the quantitative analysis of compositional models, an approach that allows one to tackle large state spaces is needed. When the models are characterised by underlying continuous time Markov chains (e.g., stochastic Petri nets, Performance Evaluation Process algebra PEPA) productform theory may be successfully applied. Informally, productforms aim at studying the model properties in steadystate starting from the analysis of its isolated components which are opportunely "parametrised" in order to take into account the interactions with the remaining parts of the model.
After introducing productform theory in stochastic process algebra domain, the talk will address the problem of deciding if productform conditions are satisfied by the composition of a set of components and how the parameterisation of these components can be achieved. Special attention will be devoted to the automation of these steps even in cases of models with infinite state spaces. The Iterative Numerical Algorithm for Productforms will be presented. Concluding remarks will consider the problem of the computation of the normalising constant and productform approximations.
 Jaco van de Pol, University of Twente
Title: Symbolic Manipulation of Markov Automata
Abstract: Markov automata combine nondeterministic choice, probabilistic choice, and stochastic delays, and come with a natural notion of parallel composition. Since these automata generalize labeled transition systems and both discretetime and continuoustime Markov Chains, they provide a rich model of computation.
We will present the process algebra MAPA for specifying Markov Automata in a symbolic manner. Specifications in MAPA can be very concise, due to parallel composition and the use of data types. MAPA specifications can be transformed into a linear process format, which is an excellent basis for symbolic transformation and optimization of Markov Automata.  Mirco Tribastone, LudwigMaximiliansUniversität München
Title: Exact Aggregation for Fluid Process Algebra Models
Abstract: Recent research in stochastic process algebra has led to efficient fluid approximation techniques obtained by aggregating large populations of sequential components into a single continuousstate variable represented as an ordinary differential equation (ODE). In this talk I will show that, when aggregation is performed higher up in the syntax tree of a model  i.e., when one is interested in replicas of composite processes  the resulting ODE system does not scale well with population sizes. I will present two techniques to tackle this problem. The first one is a modeltomodel transformation at the processalgebra level. It converts a model with a large ODE system into another one whose size is independent from all population levels, but whose solution is related exactly to that of the original system. Simple syntactic checks are a necessary condition for this transformation to be carried out. The second technique enlarges the class of models amenable to exact aggregation. It performs a transformation directly at the level of the underlying ODE system, which is induced by a novel notion of behavioural equivalence for process algebra with fluid semantics.