On distributed stochastic logics for mobile systems

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish
Title of host publicationLogic, Language, Information, and Computation
Subtitle of host publication21st International Workshop, WoLLIC 2014, Valparaíso, Chile, September 1-4, 2014. Proceedings
EditorsUlrich Kohlenbach, Pablo Barceló, Ruy de Queiroz
Number of pages11
ISBN (Electronic)9783662441459
ISBN (Print)9783662441442
Publication statusPublished - 2014
Event21st International Workshop, WoLLIC 2014 - Valparaiso, Chile
Duration: 1 Sept 20144 Sept 2014

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Workshop21st International Workshop, WoLLIC 2014
Internet address


Dive into the research topics of 'On distributed stochastic logics for mobile systems'. Together they form a unique fingerprint.

Cite this