Parameterized metatheory for continuous Markovian logic

Kim G. Larsen, Radu Mardare, Claus Thrane

Research output: Contribution to journalConference articlepeer-review

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.
Original languageEnglish
Pages (from-to)33-47
Number of pages15
JournalElectronic Proceedings in Theoretical Computer Science
Volume103
DOIs
Publication statusPublished - 14 Dec 2012
EventQuantities in Formal Methods - QFM 2012 - Paris, France
Duration: 28 Aug 201228 Aug 2012

Keywords

  • classic metalogical framework
  • boolean operators
  • Markov processes
  • continuous Markovian logic (CML)
  • stochastic bisimulation of Markov processes
  • metatheorems
  • decidability
  • weak completeness
  • finite model property

Fingerprint

Dive into the research topics of 'Parameterized metatheory for continuous Markovian logic'. Together they form a unique fingerprint.

Cite this