Continuous Markovian logic - From complete axiomatization to the metric space of formulas

Luca Cardelli, Kim G. Larsen, Radu Mardare

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

9 Citations (Scopus)

Abstract

Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some meta-properties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.

LanguageEnglish
Title of host publicationComputer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011
Pages144-158
Number of pages15
Volume12
DOIs
Publication statusPublished - 1 Dec 2011
Event25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL - Bergen, Norway
Duration: 12 Sep 201115 Sep 2011

Conference

Conference25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL
CountryNorway
CityBergen
Period12/09/1115/09/11

Fingerprint

Markov processes
Random variables
Semantics
Acoustic waves

Keywords

  • axiomatization
  • Markov processes
  • metric semantics
  • probabilistic logic

Cite this

Cardelli, L., Larsen, K. G., & Mardare, R. (2011). Continuous Markovian logic - From complete axiomatization to the metric space of formulas. In Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011 (Vol. 12, pp. 144-158) https://doi.org/10.4230/LIPIcs.CSL.2011.144
Cardelli, Luca ; Larsen, Kim G. ; Mardare, Radu. / Continuous Markovian logic - From complete axiomatization to the metric space of formulas. Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011. Vol. 12 2011. pp. 144-158
@inproceedings{0f6c86ea2f4a441cab34201911465e78,
title = "Continuous Markovian logic - From complete axiomatization to the metric space of formulas",
abstract = "Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some meta-properties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.",
keywords = "axiomatization, Markov processes, metric semantics, probabilistic logic",
author = "Luca Cardelli and Larsen, {Kim G.} and Radu Mardare",
year = "2011",
month = "12",
day = "1",
doi = "10.4230/LIPIcs.CSL.2011.144",
language = "English",
isbn = "9783939897323",
volume = "12",
pages = "144--158",
booktitle = "Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011",

}

Cardelli, L, Larsen, KG & Mardare, R 2011, Continuous Markovian logic - From complete axiomatization to the metric space of formulas. in Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011. vol. 12, pp. 144-158, 25th International Workshop on Computer Science Logic, CSL 2011/20th Annual Conference of the European Association for Computer Science Logic, EACSL, Bergen, Norway, 12/09/11. https://doi.org/10.4230/LIPIcs.CSL.2011.144

Continuous Markovian logic - From complete axiomatization to the metric space of formulas. / Cardelli, Luca; Larsen, Kim G.; Mardare, Radu.

Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011. Vol. 12 2011. p. 144-158.

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - Continuous Markovian logic - From complete axiomatization to the metric space of formulas

AU - Cardelli, Luca

AU - Larsen, Kim G.

AU - Mardare, Radu

PY - 2011/12/1

Y1 - 2011/12/1

N2 - Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some meta-properties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.

AB - Continuous Markovian Logic (CML) is a multimodal logic that expresses quantitative and qualitative properties of continuous-space and continuous-time labelled Markov processes (CMPs). The modalities of CML approximate the rates of the exponentially distributed random variables that characterize the duration of the labeled transitions. In this paper we present a sound and complete Hilbert-style axiomatization of CML for the CMP-semantics and prove some meta-properties including the small model property. CML characterizes stochastic bisimulation and supports the definition of a quantified extension of satisfiability relation that measures the compatibility of a model and a property. Relying on the small model property, we prove that this measure can be approximated, within a given error, by using a distance between logical formulas.

KW - axiomatization

KW - Markov processes

KW - metric semantics

KW - probabilistic logic

UR - http://www.scopus.com/inward/record.url?scp=84865047468&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.CSL.2011.144

DO - 10.4230/LIPIcs.CSL.2011.144

M3 - Conference contribution book

SN - 9783939897323

VL - 12

SP - 144

EP - 158

BT - Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011

ER -

Cardelli L, Larsen KG, Mardare R. Continuous Markovian logic - From complete axiomatization to the metric space of formulas. In Computer Science Logic 2011 - 25th International Workshop/20th Annual Conference of the EACSL, CSL 2011. Vol. 12. 2011. p. 144-158 https://doi.org/10.4230/LIPIcs.CSL.2011.144