Mardare, Radu; Cardelli, Luca; Larsen, Kim G. Continuous Markovian logics – axiomatization and quantified metatheory. (English) Zbl 1261.03088 Log. Methods Comput. Sci. 8, No. 4, Paper No. 19, 28 p. (2012). Summary: 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 allow us to prove two robustness theorems for the logic stating that one can perturb formulas and maintain “approximate satisfaction”. Cited in 5 Documents MSC: 03B45 Modal logic (including the logic of norms) 60J25 Continuous-time Markov processes on general state spaces 68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) Keywords:probabilistic modal logic; stochastic modal logic; axiomatization; Markov processes; metric semantics; finite model property; stochastic bisimilarity PDFBibTeX XMLCite \textit{R. Mardare} et al., Log. Methods Comput. Sci. 8, No. 4, Paper No. 19, 28 p. (2012; Zbl 1261.03088) Full Text: DOI arXiv