Continuous Markovian Logics: Axiomatization and Quantified Metatheory

Radu Iulian Mardare, Luca Cardelli, Kim Guldstrand Larsen

Research output: Contribution to journalJournal articleResearchpeer-review

10 Citations (Scopus)


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".
Original languageEnglish
JournalLogical Methods in Computer Science
Issue number4
Pages (from-to)1-29
Publication statusPublished - 29 Nov 2012


Dive into the research topics of 'Continuous Markovian Logics: Axiomatization and Quantified Metatheory'. Together they form a unique fingerprint.

Cite this