Tag Archives: Process Algebras

30/11/2017 – Talk by Ludovica Luisa Vissat

Title: Modelling of spatial stochastic systems and analysis of their spatio-temporal properties
Time: 13:00
Location: Meeting room, Ed. Zeta
Type: Research Result
Speaker: Ludovica Luisa Vissat
Abstract: In my talk I will give an overview of my PhD research work. We have initially developed a novel process algebra, specifically tailored for modelling ecological systems, and more generally for spatial stochastic systems. These systems can be seen as a collection of agents that can interact and are spatially located. To analyse properties of the dynamics of these stochastic systems, we worked with spatio-temporal logics and statistical model checking.

We introduced the novel Three-Valued Spatio-Temporal Logic, which extends the available analysis, looking at the spatio-temporal evolution of the satisfaction probabilities of given logical formulas, estimated through statistical model checking. I will present different case studies during the talk, to show various applications of our modelling language and spatio-temporal analysis.

08/11/2016 – Talk by Filippo Cavallin

Title: Multi-Step Discrete Time Process Algebra (MuPA)
Time: 13:00
Location: Meeting room, Building Zeta
Type: Research Result
Speaker: Filippo Cavallin
We consider Discrete Time Markov Chains with synchronous behaviour, i.e. models in which multiple events may occur at each recorded time in the model. This is based on a conceptual model in which the discrete times are sampling points when the system is observed and at each instant all events that have occurred since the previous observation point will be noted. We propose the first process algebra which is capable of capturing such systems and demonstrate its application to discrete time queues both in isolation and forming networks.

10.01.2013 – Talk by Giovanni Bernardi

Title: Testing preorders for clients and peers

Date: 10/01/2012
Time: 1:00 pm
Location: Sala riunioni
Type: research talk
Speaker: Giovanni Bernardi (Trinity College, Dublin)

The must testing is a formalism that let us reason on the safety of  computations performed by two communicating parties; typically a  client (test) and a server (process). By using the must testing one can define three refinements that state when it is safe to replace servers, clients, or peers.
In this talk we explain the classic semantic characterisation of the must preorder for servers, and then we show how to generalise so as to characterise also the preorders for clients and peers.

12.12.2012 – Tutorial by Stefano Calzavara

Title: An introduction to stochastic process algebras and quantitative security analysis

Date: 12/12/2012
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.