Radu Mardare ; Luca Cardelli ; Kim G. Larsen - Continuous Markovian Logics - Axiomatization and Quantified Metatheory

lmcs:937 - Logical Methods in Computer Science, November 29, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:19)2012
Continuous Markovian Logics - Axiomatization and Quantified MetatheoryArticle

Authors: Radu Mardare ; Luca Cardelli ORCID; Kim G. Larsen

    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".


    Volume: Volume 8, Issue 4
    Published on: November 29, 2012
    Imported on: March 4, 2012
    Keywords: Computer Science - Logic in Computer Science,F.4.1, G.3

    8 Documents citing this article

    Consultation statistics

    This page has been seen 1424 times.
    This article's PDF has been downloaded 435 times.