Continuous Markovian Logics: Axiomatization and Quantified Metatheory

Radu Iulian Mardare, Luca Cardelli, Kim Guldstrand Larsen

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

10 Citationer (Scopus)

Abstrakt

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".
OriginalsprogEngelsk
TidsskriftLogical Methods in Computer Science
Vol/bind8
Udgave nummer4
Sider (fra-til)1-29
ISSN1860-5974
DOI
StatusUdgivet - 29 nov. 2012

Fingeraftryk

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

Citationsformater