Continuous Markovian Logics: Axiomatization and Quantified Metatheory

Radu Iulian Mardare, Luca Cardelli, Kim Guldstrand Larsen

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

10 Citationer (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".
TidsskriftLogical Methods in Computer Science
Udgave nummer4
Sider (fra-til)1-29
StatusUdgivet - 29 nov. 2012


Dyk ned i forskningsemnerne om 'Continuous Markovian Logics: Axiomatization and Quantified Metatheory'. Sammen danner de et unikt fingeraftryk.