Continuous Markovian logics axiomatization and quantified metatheory

Radu Mardare, Luca Cardelli, Kim G. Larsen

Research output: Contribution to journalArticle

10 Citations (Scopus)

Abstract

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
Pages (from-to)1-28
Number of pages28
JournalLogical Methods in Computer Science
Volume8
Issue number4
DOIs
Publication statusPublished - 29 Nov 2012

Keywords

  • axiomatization
  • Markov processes
  • metric semantics
  • probabilistic and stochastic modal logics

Fingerprint Dive into the research topics of 'Continuous Markovian logics axiomatization and quantified metatheory'. Together they form a unique fingerprint.

  • Cite this