On distributed stochastic logics for mobile systems

We introduce a family of logics for expressing and reasoning about stochastic properties over mobile distributed systems. More specifically, to reason about state properties, action sequences, location-based properties and differentiate between local and global object-based behaviour, we define an ASMC ⁺ extending an action and state-based Markov chain with object and location labels. We introduce a distributed stochastic logic DSL interpreted over ASMC ⁺ s. For an ASMC ⁺ model M, we define quotient structures equivalent to M which induce sublogics over DSL. The logics include a global stochastic logic GSL and local stochastic logics LSL for locations in the system. In general, the logics can be used to capture different quantitative dependability properties for distributed mobile systems. We point out that the interpretation of the sublogics over equivalence preserving state space aggregations brings considerable advantages for verification.