Continuous Markovian Logics - Axiomatization and Quantified Metatheory

TL;DR

This paper introduces axiomatizations for Continuous Markovian Logic (CML), a logic for continuous-time Markov processes, and explores its properties, including bisimilarity characterization and robustness to perturbations.

Contribution

It provides the first complete axiomatizations for CML and develops a quantified extension to measure model-property compatibility.

Findings

CML characterizes stochastic bisimilarity.

The logic supports approximate satisfaction robustness.

Canonical models and finite model property are established.

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