Mardare, Radu Iulian1; Cardelli, Luca6; Larsen, Kim Guldstrand3
1 Department of Computer Science, The Faculty of Engineering and Science, Aalborg University, VBN2 The Faculty of Engineering and Science, Aalborg University, VBN3 CISS - Center for Embedded Software Systems, The Faculty of Engineering and Science, Aalborg University, VBN4 Distributed Systems and Semantics, The Faculty of Engineering and Science, Aalborg University, VBN5 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN6 Microsoft Research Cambridge
Axiomatization and Quantified Metatheory
Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-time labelled Markov processes with arbitrary (analytic) state-spaces, henceforth called continuous Markov processes (CMPs). The modalities of CML evaluate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions of a CMP. In this paper we present weak and strong complete axiomatizations for CML and prove a series of metaproperties, including the finite model property and the construction of canonical models. CML characterizes stochastic bisimilarity and it supports the definition of a quantified extension of the satisfiability relation that measures the "compatibility" between a model and a property. In this context, the metaproperties allows us to prove two robustness theorems for the logic stating that one can perturb formulas and maintain "approximate satisfaction".
Logical Methods in Computer Science, 2012, Vol 8, Issue 4, p. 1-29