Abstract:
When modelling distributed systems it is useful to have an explicit notion of location, local clocks, timed migration and interaction. After introducing the timed distributed pi-calculus, we introduced and studied a process algebra called TiMo having exactly these features. A probabilistic extension of TiMo assigns probabilities to the transitions that describe the behaviour of TiMo networks by solving the nondeterminism involved in the movement and in the communication of processes, as well as in the selection of active locations. The main reason for creating a probabilistic extension of TiMo is to gain the ability to verify quantitative properties of TiMo distributed systems networks, such as the probability that a certain transient or steady-state behaviour occurs. It is natural to have a probabilistic temporal logic for expressing such properties over networks of located processes. Unfortunately, quantitative logics as PCTL or aPCTL are not immediately compatible with all or most of the distinguishing features of TiMo. As a result, we define a novel logic called PLTM (Probabilistic Logic for Timed Mobility). The new probabilistic temporal logic PLTM is able to describe certain aspects that are not commonly found in other logics, such as the ability to check properties which make explicit reference to specific locations and processes, to impose temporal constraints over local clocks (finite or infinite upper bounds, for each location independently), to define complex action guards over multisets of actions and properties for transient and steady-state behaviours. Finally, we present a verification algorithm for PLTM, and determine its time complexity. Given that PLTM operates at the level of discrete-time Markov chains, it can also be applied to other process algebras which involve locations, timers, process movements and communications.