technical report Continuous Markovian Logic


In this paper we introduce Continuous Markovian Logic (CML), a simple formalism inspired by coalgebraic logic, to characterize the bisimulation of Markov processes having continuous state space and continuous temporal evolution (CMPs). The alternative, continuous stochastic logic (CSL), has expressive power which comes at the price of a complicated two-layer semantics and requires a complex mathematical apparatus for calculating the probabilities of computational paths in time. CML focuses on the rates of the exponentially distributed random variables that characterize the duration of transitions, instead of explicitly expressing time-dependent probabilistic information as in the case of CSL. Thus, CML exploits the fact that the probabilistic-temporal information is encapsulated in the rates. We prove that the negation-free fragment of CML is already suficient to completely characterize bisimulation of CMPs. We also show a sound-complete axiomatization of CML and demonstrate that, unlike CSL, it enjoys the small model property.

Paper Details


R. Mardare,  L. Cardelli