Parameterized Metatheory for Continuous Markovian Logic

TL;DR

This paper develops a comprehensive Boolean logical framework for continuous Markovian logic, enabling metric behavioral analysis of Markov processes with arbitrary state spaces and continuous-time transitions, including bisimulation and observational preorders.

Contribution

It introduces an epsilon-parameterized metatheory for CML using a complete Boolean framework, extending previous intuitionistic approaches and supporting metric behavioral analysis.

Findings

Established sound and complete axiomatization for epsilon-satisfiability and epsilon-provability.

Proved decidability, weak completeness, and finite model property for the framework.

Unified Boolean framework supports analysis of stochastic bisimulation and behavioral pseudometrics.

Abstract

This paper shows that a classic metalogical framework, including all Boolean operators, can be used to support the development of a metric behavioural theory for Markov processes. Previously, only intuitionistic frameworks or frameworks without negation and logical implication have been developed to fulfill this task. The focus of this paper is on continuous Markovian logic (CML), a logic that characterizes stochastic bisimulation of Markov processes with an arbitrary measurable state space and continuous-time transitions. For a parameter epsilon>0 interpreted as observational error, we introduce an epsilon-parameterized metatheory for CML: we define the concepts of epsilon-satisfiability and epsilon-provability related by a sound and complete axiomatization and prove a series of "parameterized" metatheorems including decidability, weak completeness and finite model property. We also prove results regarding the relations between metalogical concepts defined for different parameters. Using this framework, we can characterize both the stochastic bisimulation relation and various observational preorders based on behavioural pseudometrics. The main contribution of this paper is proving that all these analyses can actually be done using a unified complete Boolean framework. This extends the state of the art in this field, since the related works only propose intuitionistic contexts that limit, for instance, the use of the Boolean logical implication.