MLQA 2012

Joint Workshop on Compositional Modelling and Analysis of Quantitative Systems September 8, 2012 University of Edinburgh

---

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 Newcastle-upon-Tyne 4-7th 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 product-forms
• Jaco van de Pol, University of Twente
  Symbolic manipulation of markov automata
• Mirco Tribastone, Ludwig-Maximilians-Universitä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 on-going 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 time-bounded 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 product-forms
  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-) product-form theory may be successfully applied. Informally, product-forms aim at studying the model properties in steady-state 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 product-form theory in stochastic process algebra domain, the talk will address the problem of deciding if product-form 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 Product-forms will be presented. Concluding remarks will consider the problem of the computation of the normalising constant and product-form approximations.
  
  
• Jaco van de Pol, University of Twente
  Title: Symbolic Manipulation of Markov Automata
  Abstract: Markov automata combine non-deterministic choice, probabilistic choice, and stochastic delays, and come with a natural notion of parallel composition. Since these automata generalize labeled transition systems and both discrete-time and continuous-time 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, Ludwig-Maximilians-Universitä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 continuous-state 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 model-to-model transformation at the process-algebra 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.

---

Minutes

Minutes of MLQA 2012 is avaliable here.