10.4230/LIPICS.CSL.2011.144
Cardelli, Luca
Luca
Cardelli
Larsen, Kim G.
Kim G.
Larsen
Mardare, Radu
Radu
Mardare
Continuous Markovian Logic - From Complete Axiomatization to the Metric Space of Formulas
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
probabilistic logic
axiomatization
Markov processes
metric semantics
Bezem, Marc
Marc
Bezem
2011
2011-08-31
2011-08-31
2011-08-31
en
urn:nbn:de:0030-drops-32281
10.4230/LIPIcs.CSL.2011
978-3-939897-32-3
1868-8969
10.4230/LIPIcs.CSL.2011
LIPIcs, Volume 12, CSL 2011
Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL
2013
12
14
144
158
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Bezem, Marc
Marc
Bezem
1868-8969
Leibniz International Proceedings in Informatics (LIPIcs)
2011
12
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
15 pages
560800 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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 metaproperties 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.
LIPIcs, Vol. 12, Computer Science Logic (CSL'11) - 25th International Workshop/20th Annual Conference of the EACSL, pages 144-158