Date: Wed 14 Feb
Time: 15.00
Place: room 214

Speaker: Luigi Campora
Title: Towards a model for distributed reactive systems

Abstract. We aim at giving a contribution towards a formal semantic framework for distributed reactive systems based on labeled transition systems. Lts's are a well-suited and largely-accepted model for reactive systems for what concerns the modeling of reactivity; yet, lts's miss the description of distribution, say the way the activity is spread among spatially-separated components. We address the topic of adding suitable ingredients to lts's in order to properly describe the notion of component. As a preliminary step in our work towards a complete model for distributed reactive systems we introduce distributed labeled transition system (dlts), a refinement of lts's where the formal description of the notion of component is factorized into three different ingredients, namingly architectural structure, behavioural structure, and identity. We equip dlts's with a set of strong bisimulations semantics arising as instances of two general schemes,called global and local, corresponding to two different approaches to the notion of simulation among components. These semantics can be ordered in two strictly increasing hierarchies, and each one can be qualified w.r.t. the degree of observed distribution. Depending upon the way the scheme is instantiated, one can have semantics preserving behavioural structure, sharing, strong or weak fairness. In the last few years, a lot of work has been done for equipping CCS-like calculi with non-interleaving observational semantics; location equivalence can be considered as the major example. In this setting, distributed aspects of concurrent computations has been studied mainly from a syntactic point of view, by exploiting the concrete information provided by the rules of the SOS system. We compare our semantics with some of these location-based semantics, on the ground on a sub-calculus of CCS.