RECORD
Parameterized Metatheory for Continuous Markovian Logic
Logic in Computer Science · Submitted 17 Dec 2012
abstract compiled · 2026-09-23 · no language-model review
The authors' main claim The main contribution of this paper is proving that all these analyses can actually be done using a unified complete Boolean framework.
The compiled record
The paper's own sentences, arranged. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.
Open the compiled record
The abstract, sentence by sentence
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.
background contribution method result interpretation main claim
| # | sentence | role | the authors' own work | states the main conclusion | strength |
|---|---|---|---|---|---|
| s0 | 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. | contribution 0.81 | 0.93 | 0.39 | asserted 1.00 |
| s1 | Previously, only intuitionistic frameworks or frameworks without negation and logical implication have been developed to fulfill this task. | gap 0.94 | 0.03 | 0.04 | asserted 1.00 |
| s2 | 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. | background 0.78 | 0.21 | 0.04 | asserted 1.00 |
| s3 | 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. | contribution 0.81 | 0.97 | 0.12 | asserted 1.00 |
| s4 | We also prove results regarding the relations between metalogical concepts defined for different parameters. | result 0.73 | 0.94 | 0.04 | asserted 1.00 |
| s5 | Using this framework, we can characterize both the stochastic bisimulation relation and various observational preorders based on behavioural pseudometrics. | result 0.61 | 0.91 | 0.07 | asserted 0.74 |
| s6 | The main contribution of this paper is proving that all these analyses can actually be done using a unified complete Boolean framework. | contribution 1.00 | 0.93 | 0.96 | asserted 1.00 |
| s7 | 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. | interpretation 0.51 | 0.23 | 0.17 | asserted 1.00 |
What was examined, and what was not
- arXiv listing abstract v1
- full text
- figures and tables
- references and citing sentences
- relations to other papers
- P abstract
- S sections
- T body sentences
- C citations
- R cross-paper relations
The paper
Original 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.
Human review
Discussion
Know something about this paper? Leave a comment, or highlight any passage above to comment on it.