Tutorial T5
T5 tutorial 1 - Networks of Processes: Modeling, Analysis, and Optimization
Peter Kemper
(Univ. of Dortmund, Germany)
Duration: 90 minutes
Modelling with processes has a long tradition in modelling computer and communication systems and has recently gained a lot of attention in modelling software processes as well as manufacturing, production and logistic systems. In this tutorial, we discuss modelling with processes, in particular, how to handle the complexity of large models by an appropriate hierarchical structure and how to handle the role of mobile resources that are available with time and location constraints. Techniques for verification and validation of models are considered which include innovative visualization aids and techniques for debugging complex simulation models. We discuss discrete event simulation for performance, performability measures but also for measuring costs, for instance, by following an activity based costing approach. Finally, we consider issues on the combination of optimization with simulation to support decision making in the model-based design of systems.
T5 tutorial 2 - Equivalences for Markovian Process Calculi
Marco Bernardo
(Univ. of Urbino, Italy)
Duration: 90 minutes
Several Markovian process calculi have been proposed in the literature, all of which come equipped with a notion of equivalence that aims at relating process terms that behave the same both from the functional and the performance viewpoint.

Most of the equivalences for Markovian process calculi are based on the bisimulation approach, while only recently alternative approaches based on testing scenarios and traces have been considered.

Such Markovian equivalences can be compared on the basis of various criteria:

  • exactness of the CTMC-level aggregation they induce;
  • congruence property;
  • sound and complete axiomatization;
  • logical characterization;
  • efficient algorithms to check for them.

After recalling the basics of Markovian process calculi, in this tutorial we present several variants of Markovian bisimulation equivalence, then we compare it to two more recent non-branching-time alternatives called Markovian testing equivalence and Markovian trace equivalence.

Web Maintenance Person.