Title: On the solution of cooperating stochastic models
Location: Meeting room
Type: Research Result
Speaker: Gian-Luca dei Rossi
Stochastic models are widely used in the performance evaluation community. In particular, Markov processes, and more precisely, Continuous Time Markov Chains (CTMCs), often serve as underlying stochastic processes for models written in higher-level formalisms, such as Queueing Networks, Stochastic Petri Nets and Stochastic Process Algebras.. While compositionality, i.e., the ability to express a complex model as a combination of simpler components, is a key feature of most of those formalisms, CTMCs, by themselves, don’t allow for mechanisms to express the interaction with other CTMCs. In order to mitigate this problem various lower-level formalisms have been proposed in literature, e.g., Stochastic Automata Networks (SANs), Communicating Markov Processes, Interactive Markov chains and the labelled transition systems derived from PEPA models.
However, while the compositionality of those formalism is a useful property which makes the modelling phase easier, exploiting it to get solutions more efficiently is a non-trivial task. Ideally one should be able to either detect a product-form solution and analyse the components in isolation or, if a product form cannot be detected, use other techniques to reduce the complexity of the solution, e.g., reducing the state space of either the single components or the joint process. Both tasks raised considerable interest in the literature, e.g., the RCAT theorem for the product-form detection or the Strong Equivalence relation of PEPA to aggregate states in a component-wise fashion.This talk deals with the aforementioned problem of efficiently solving complex Markovian models expressed in term of multiple components. We restrict our analysis to models in which components interact using an active-passive semantics. The main contributions rely on automatic product-forms detection, in components-wise lumping of forward and reversed processes and in showing that those two problems are indeed related, introducing the concept of conditional product-forms.
Title: Separable solution for interacting stochastic automata
Time: 1:30 pm
Location: Sala riunioni
Type: research talk
Speaker: Maria Grazia Vigliotti (Imperial College, London)
We present product-form solutions from the point of view of stochastic process algebra. In previous work we have shown how to derive
product-form solutions for a formalism called Labelled Markov Automata (LMA). LMA are very useful as their relation with the Continuous Time Markov Chains is very direct. The disadvantage of using LMA is that the proofs of properties are cumbersome. In fact, in LMA it is not possible to use the inductive structure of the language in a proof. In this paper we consider a simple stochastic process algebra that has the great advantage of simplifying the proofs. This simple language has been inspired by PEPA, however,
detailed analysis of the semantics of cooperation will show the differences between the two formalisms. It will also be shown that the semantics of the cooperation in process algebra influences the correctness of the derivation of the product-form solutions.
Title: An introduction to stochastic process algebras and quantitative security analysis
Time: 3:00 pm
Location: Sala riunioni
Type: review of literature
Speaker: Stefano Calzavara (Ca’ Foscari, Venice)
Stochastic process algebras are a popular and convenient specification tool, which have proven successful in many applications from the areas of performance modeling, bioinformatics, and security. However, approaching the world of stochastic process algebras is a nontrivial task, since the very foundations of such models are rather peculiar and the well-known formal machinery of classical (non-deterministic) process algebras does not properly fit them. In this talk we analyze stochastic process algebras from the point of view of the programming languages community, and we try to motivate and understand some apparently weird design choices underlying their development. We then focus on an application of stochastic process algebras to security verification and we propose a personal understanding of the challenges behind such task. We argue that, as the foundations of stochastic process algebras depart from those of classical process algebras, also the approach to their verification may probably benefit from a change of perspective.
Prerequisites: Some notions on process algebras and formal methods may help in appreciating the contents, but the seminar is self-contained.