{'fraction_non_alphanumeric': 0.036331558140294706, 'fraction_numerical': 0.008070049335119418, 'mean_word_length': 4.546937296121783, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Parameterized Metatheory for Continuous Markovian Logic

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.


Introduction
Stochastic models have successfully been used to describe the qualitative and quantitative behavior of systems in many natural and artificial domains. The problems addressed in this paper refer to the most general models of Markov processes, defined for arbitrary (analytic) state-spaces and continuous-time transitions, henceforth continuous Markov processes (CMPs); they subsume well-known models such as continuous-time Markov chains and labelled Markov processes and for this reason our work can be simply instantiated for these particular models. CMPs have been initially introduced by Desharnais and Panangaden in [DP03]. In this paper, for technical reasons, we use the definition of CMPs proposed by the first two authors and Cardelli in [CLM11a], which exploits an equivalence between the definitions of Harsanyi type spaces [MV04] and a coalgebraic view of labelled Markov processes [dVR99] proved, for instance, by Doberkat in [Dob07].
In this paper the class of CMPs define the semantics for Continuous Markovian Logic (CML) [CLM11a,CLM11b]. This is a multimodal logic endowed with modalities L r , M r for r ∈ Q + , similar to the ones used by the Aumann system [Aum99], that approximates the transition rates. For instance, a process satisfies L r φ if the rate of its transition from the initial state to a state satisfying φ is at least r. In [CLM11a] it has been proved that this logic characterizes the stochastic bisimulation of CMPs.
Despite the elegant theories supporting the concepts of stochastic and probabilistic bisimulations and their relation to logics [LS91], these concepts remain too strict for applications. In modelling, the values of the rates or probabilities are often approximated and consequently, one is interested to know whether two processes that differ by a small amount in real-valued parameters show similar (not necessarily identical) behaviours. In such cases, instead of a bisimulation relation, one needs a metric concept to estimate the degree of similarity of two systems in terms of their behaviours. The metric theory for Markov processes was initiated by Desharnais et al. [D+04] and has been greatly developed and explored by van Breugel, Worrell and others [vBW01,vB+03]. Similar notions have been proposed in literature for less general models. Bringing with them notions such as the point-wise simulation distance defined in [JS90] for discrete probabilistic systems, and the discounted distances proposed in [AHM03,AFS09] for weighted systems, and of the quantified similarities of timed systems studied in [MHP05] and [TFL10] (see also [Thr11] for an overview).
One way of defining these behavioural distances was proposed by Kozen [Koz85] and consists in replacing the classic logical framework used to encode properties of processes with a non-classical realvalued framework that will interpret logical formulae as functional expressions mapping states to reals. In this way, we get a relaxation of the satisfiability relation which is replaced by a function that reports the "degree of satisfiability" between a Markov process and a logical property. This further induces a behavioural pseudometric on processes with the stochastic bisimulation as its kernel and measuring the distance between processes in terms of their behavioural similarity. Such formalisms have since been proposed for Markov systems by Desharnais, Panangaden and others [D+04,Pan09].
It was hoped that these metrics would provide a quantitative alternative to logic, but this did not happen. One reason could originate in the fact that all this "metric reasoning" focused exclusively on the semantics of the logic while a syntactic or a metalogical counterpart did not develop until recently. Such a logical perspective on distance was proposed by the first two authors of this paper and Cardelli in [CLM11a], where it was emphasized that, in the context of a completely axiomatized logic, the semantic distance between Markovian processes implicitly induces, via Hausdorff metrics, a distance between logical properties that can be interpreted as a measure of provability for CML. On this line, [CLM11a] and [CLM11b] contain the open ideas of a research program that we have followed ever since. This research aims to understand the relation between the pseudometric space of Markov processes and the pseudometric space of logical formulae i.e., the relation between the measure of similarity for Markov processes and the measure of provability in a corresponding stochastic/probabilistic logic. Eventually, in [LMP12a], the first two authors in collaboration with Prakash Panangaden have identified a metric analog of Stone duality that relates the two pseudometric spaces and in [LMP12b] we have studied how convergence in the open ball topologies induced by the two pseudometrics "agree to the limit".
However, we have yet to clarify what the kernel of the distance between logical formulae is. It was shown in [LMP12b] that it is possible to have formulae at distance 0 that are not logically equivalent, and we have characterized this kernel for some limited fragments of CML. But the full picture has not been yet achieved. One reason for this difficulty originates from the fact that we have no pure metalogical definition of this distance, as it is always implicitly obtained from the definition of the behavioural pseudometrics, hence it depends of the semantics. This is exactly what we achieve in this paper: a metalogical definition of the behavioural distance. This paper is a step forward in the process of understanding this distance from a logical perspective. We define a parameterized metatheory for CML, where the parameter ε ≥ 0 is interpreted as an observational error which allows us to express properties approximating the behavior of a given CMP. This metatheory consists in defining an ε-semantics, i.e., ε-satisfiability relation denoted | = ε , and to develop a complete Hilbert-style axiomatization for a corresponding concept of ε-provability, denoted ε . The classic semantics and provability relation of CML are, in this context, the 0-semantics and 0-proof theory.
This parametric metatheory allows us to transfer logical properties between various semantics defined for different parameters. For instance, we can translate 0-satisfiability into ε-satisfiability and reverse, or 0-provability into ε-provability and reverse using appropriate encodings. Exactly this allows one to see the behavioural pseudometrics from a logical perspective. We show that the distance between two CMPs m 1 and m 2 can, in fact, be defined by the infimum of the set of values ε such that for any CML formula φ, We develop the parametric metatheory as a classic metatheory and in addition to the sound-complete axiomatization we prove a series of metatheorems including an ε-deduction theorem, a ε-finite model property and some ε-decidability results for CML.
The major contribution of this paper consists in the fact that this entire development respects the classic Boolean restrictions. So fare all attempts of realizing Kozen's idea [Koz85] and defining a quantitative version of the satisfiability relation, have faced noticeable problems related to the treatment of negation. Often in the papers treating this argument, negation is either eliminated, restricted to atomic propositions or considered in a non-Boolean context [FGK10,FLT10,DLT08]. This restriction is an impediment for the use of classic reasoning. For instance in [DLT08], the definition of ε-satisfiability contains the following rules defined for an arbitrary Markov process m: is the probability of a transition from m to a state in the set M. Observe that the rule for negation requires to transport information from "ε-semantics" to "−ε-semantics" and that it is obviously non-Boolean. For instance, in the case θ(m, φ ε ) = δ one can prove, using the previous rules, that for In other words, the logic is inconsistent if it is interpreted in a Boolean context. In the light of this observation, one can see the real contribution of our paper. We show that it is possible to obtain the sought after behavioral distances and remain Boolean and classic to all logical levels. Of course, one can argue that an intuitionistic approach is as good for applications as the classic Boolean approach is, and we cannot argue against this. But we believe that for a deeper understanding of Markov processes and for providing a strong theoretical background for an approximation theory of Markov processes, a classic logical framework is more useful. In fact, in [LMP12a] a special Boolean algebra (called Aumann algebra) is identified with operators that corresponds to CML and we proved Stone duality results between these algebras and Markov processes. This enforces our trust that the Boolean setting is the right one for studying properties of Markov processes.
To summarize, the achievements of this work are as follows.
• We develop a parameterized metatheory for continuous Markovian logic that extends the classic metatheory. The parameter can be interpreted as observational error.
• We define the concept of ε-satisfiability and identify for it an appropriate concept of ε-provability with a sound and complete Hilbert-style axiomatization.
• We prove that classic metatheorems about CML remain true in the parametric semantics. Such properties are the weak completeness, the finite model property and decidability.
• We show that this parameterized metatheory can be used to define a behavioural pseudometric, which is a distance between CMPs that characterizes the similarity of two processes from the point of view of their behaviours.
• We identify two behavioural orders that have, in the parametric semantics, similar logical interpretations to the bisimulation in the classic semantics.

Preliminary definitions
In this section we introduce some basic notations and concepts used throughout this paper. For arbitrary sets M, N, we denote by 2 M the powerset of M, by M N their disjoint union and by [M → N] the set of functions from M to N.
A set Σ ⊆ 2 M is a σ-algebra over M if it contains M and it is closed under complement and countable union. Given a σ-algebra Σ over M, the tuple (M, Σ) is called a measurable space and the elements of Σ, measurable sets. A set Ω ⊆ 2 M is a generator for Σ if Σ is the closure of Ω under complement and countable union.
Given a measurable space (M, Σ), a function µ : Σ → R + is a measure iff µ(∅) = 0 and for any sequence The set of all measures on (M, Σ) is denoted by ∆(M, Σ). We organize ∆(M, Σ) as a measurable space by considering the σ-algebra F generated, for arbitrary S ∈ Σ and r > 0, by the sets F r We use M → N to denote the class of measurable mappings from (M, Σ) to (N, Σ ), assuming of course that Σ and Σ are clear from the context.
Central for this paper is the notion of analytic space that supports some of the main results. As properties of analytic spaces are however not used here directly, we only recall the main definitions. For detailed discussion on this topic related to Markov processes, the reader is referred to [Pan09] (Section 7.5) or to [Dob07] (Section 4.4).
A metric space (M, d) is complete if every Cauchy sequence converges in M. A Polish space is the topological space underlying a complete metric space with a countable dense subset. An analytic space is the image of a Polish space under a continuous function between Polish spaces.

Continuous Markov processes
In this section we introduce continuous Markov processes (CMPs) [CLM11a,CLM11b] which are models of stochastic systems with analytic state space and continuous-time transitions. The definition is similar to the one proposed by Desharnais and Panangaden in [DP03], but it exploits an equivalence between the definitions of Harsanyi type spaces [MV04] and a coalgebraic view of labelled Markov processes [dVR99] proved, for instance, by Doberkat in [Dob07]. However, with respect to [CLM11a,CLM11b] or to [Pan09, DEP02, Dob07], we do not consider action labels. The labels can easily be added without changing any aspects of the theory.

Bisimulation
Stochastic bisimulation for CMPs follows the line of Larsen-Skou probabilistic bisimulation [LS91,DEP02,Pan09]. Recall that Σ(R) in the next definition denotes the R-closed sets of Σ.

Definition 2 (Stochastic Bisimulation). Given a CMK
Two processes (M, m) and (M, n) are stochastic bisimilar, written m ∼ M n, if they are related by a stochastic bisimulation relation.
Observe that, for any CMK M there exist stochastic bisimulation relations: for instance, the identity relation on its support-set is such a relation. The relation ∼ M is the largest stochastic bisimulation relation.

Generators
The definition of bisimulation can be amended to focus on two particular classes of generators of the σ-algebra.
Definition 4 (Bisimulation Generators). Consider the CMK M = (M, Σ, θ) and let • The bisimulation generator of M, denoted by G M , is the closure of Θ under union and intersection.
• The extended bisimulation generator of M, denoted G M , is the closure of Θ under union, intersection and complement.
Observe that the bisimulation generators are generators of Σ(∼) which is a sub-sigma algebra of Σ, i.e., Σ(∼) is the closure of both G M and G M under complement and countable union. This observation allows us to characterize the stochastic bisimulation from the perspective of the bisimulation generators and to propose some generalizations of the stochastic bisimulation. But more importantly, they will be instrumental later, for obtaining our results on logical characterization. • whenever (m, n) ∈ R, θ(m)(C) = θ(n)(C) for any C ∈ G M , • whenever (m, n) ∈ R, θ(m)(C) = θ(n)(C) for any C ∈ G M .

Continuous Markovian Logics
In this section we recall the continuous Markovian logic (CML) introduced and studied in [CLM11a,CLM11b]. This logic extends the probabilistic logics for discrete-time Markov processes [LS91,DEP02,Pan09] and for Harsanyi type spaces [FH94,Zho07] to stochastic domains and it characterizes the stochastic bisimulation. In addition to the Boolean operators, this logic is endowed with stochastic modal operators that approximate the rates of transitions. In the original definition, L r φ is a property of a CMP (M, m) whenever the rate of the transition from m to the class of states satisfying φ is at least r.
Definition 5 (Syntax). The set L of formulae of CML is generated by the following grammar, for arbitrary r ∈ Q + .
As usual, we work with all the Boolean operators, including ⊥ = ¬ . In addition, we isolate two useful sublanguages of L:

Parameterized Semantics: ε-satisfiability
In [CLM11a,CLM11b] the first two authors in collaboration with Cardelli defined the semantics of CML for arbitrary CMPs, henceforth the classic semantics for CML. We will take a similar approach in this paper with the difference that the satisfiability relation is parameterized. Thus, for each rational ε ≥ 0, we introduce an ε-semantics that provides an approximation of the classic semantics. The ε-semantics can be seen as an "approximation from below" of the classic semantics: while L r φ is interpreted at m as "the rate of the transitions from m to the class of the states satisfying φ is at least r", in the ε-semantics it means that "the rate of the transitions from m to the class of the states satisfying φ is at least r − ε". In this way one can encode observational errors in the logic. Unlike the similar approach of [DLT08], we propose a Boolean semantics.
• m | = ε always, • m | = ε ¬φ iff it is not the case that m | = ε φ, Notice that the classic semantics for CML introduced in [CLM11a, CLM11b] is nothing else but 0-semantics, since | = 0 = | =.  The semantics of L r φ is well defined only if φ ε is measurable. This is guaranteed by the fact that θ is a measurable mapping between (M, Σ) and (∆(M, Σ), F), as proved in the next lemma.
We extend the classical metalogical concepts to the parametric metatheory.
For notational convenience we will write m | = ε φ when it is not the case that m | = ε φ, and use | = in place of | = 0 . The proof of the previous lemma reveals a deeper result connecting the ε-semantics, if we involve our notion of bisimulation generators.

Corollary 1. For any rational
The major advantage that the parametric semantics provides is that one can handle in parallel properties from different semantics and, for instance, can prove (ε + ε )-satisfiability properties from properties concerning ε-satisfiability.
In what follows we establish a few such results. The first lemma establishes the relation between ε-semantics and the classic semantics.
The following counter-example shows that we cannot hope for the result to hold for negative formulae.
Notice that if ε is growing, the set φ ε is increasing when φ ∈ L + and is decreasing when φ ∈ L − . Although negation turns out to be problematic in the case of the previous lemma, we can however characterize the relation between | = ε and | = ε+ε for the entire language. To characterize completely the relation between two parametric semantics, we define a pair of dual encodings.
Definition 8. Let ε : L → L and ε : L → L be two functions on L defined as follows.
Observe that for any φ that is not of type L r ψ with r < ε, we have that φ ε ε = φ ε ε = φ. Before we turn to the main theorem of this section, we apply the previous definition to obtain a result on limits. The result may additionally be considered a form of reverse implication for Lemma 2.
We are now ready to state the main theorem of this section that establishes the relation between various parameterized semantics for the entire language L.
Theorem 2. For arbitrary φ ∈ L, From this last theorem we can derive a characterization of the relation between the classic semantics and the ε-semantics.

Parameterized Proof Theory: ε-Provability
In this section we extend the metatheory and define a parameterized proof system for our logic that corresponds to the parameterized semantics. The parameterized proof system will permit us to prove, syntactically, approximated properties of models. We should emphasize that we will not work with "approximated proofs", but with "exact proofs" about "approximated properties" and this is where the Boolean character of our metatheory plays its role.
For each rational ε ≥ 0 we introduce a notion of ε-provability denoted by ε . Table 1 contains a Hilbert-style axiomatization of ε-provability for our ε-semantics. The axioms and rules, which are considered in addition to the axiomatization of classic propositional logic, are stated for propositional variables φ, ψ ∈ L and arbitrary s, r ∈ Q + . Axiom (A1) guarantees that the rate of any transition with an ε-approximation is at least 0 + ε = ε; this encodes the fact that the real measure of any set cannot be negative. (A2) states that if a rate is at least r + s then it is at least r. (A3) and (A4) encode the additive properties of measures for disjoint sets: Table 1: The axiomatization of ε-provability for CML φ ∧ ψ ε and φ ∧ ¬ψ ε are disjoint sets of processes such that φ ∧ ψ ε ∪ φ ∧ ¬ψ ε = φ ε . The rule (R1) establishes the monotonicity of L r . In this axiomatic system we have two infinitary rules, (R2) and (R3). The first reflects the Archimedian property of rationals: if it is possible a transition from a state to a given set of states at any rate r < s, then the rate of the transition is at least s. (R3) eliminates the possibility of having transitions at infinite rates. Now we can complete the list of parametric meta-concepts initiated in Definition 7. Definition 9. A formula φ ∈ L is ε-provable, written ε φ, if either it is an instance of an axiom or it can be proved from axioms using the proof rules. A formula φ ∈ L is ε-consistent, if φ → ⊥ is not provable.
Given a set Φ ⊆ L of formulae, we say that Φ ε-proves φ, denoted by Φ ε φ, if φ can be proved from axioms and the formulae of Φ. Φ is ε-consistent if it is not the case that Φ ε ⊥.
For a sublanguage L ⊆ L, we say that Φ ∈ L is L -maximally ε-consistent if Φ is ε-consistent and no formula of L can be added to it without making it ε-inconsistent.
The next theorem states that | = ε and ε agree about the class of CMPs. As before, we will simply denote 0 by and we call to it as classic provability. Theorem 3 (Soundness and Weak Completeness). The axiomatic system of ε-provability is sound and complete for the ε-semantics, i.e., for any φ ∈ L, Proof. In [CLM11a] we have shown that in table 2 we have a sound and complete axiomatizaion of the classic provability for the classic semantics. In other words, we have proved that φ iff | = φ. Obviously, the axioms (A1)-(A4) are the ε -encodings of the axioms (B1)-(B4) and similarly (R1)-(R3) are the encodings of (S1)-(S3).
Trivial consequences of the completeness theorem, Theorem 2 and Lemma 2 are comprised in the next lemma which establishes the relation between various ε-provabilities.
The previous lemma allows us to prove a parameterized deduction theorem that establishes the frame in which one can use various ε-provabilities relations in the same proof.
The relation between the classic semantics and the ε-semantics also allows us to prove the next decidability result.
Theorem 5 (Decidability and Complexity of ε-satisfiability). The problem of deciding if an arbitrary property φ ∈ L is ε-satisfiable, i.e., if there exists a CMP m such that m | = ε φ, is decidable in Pspace.
Following the same proof line of Theorems 3 and 4 we can prove that the logic enjoys a parameterized version of finite model property.

Behavioral Properties
In the previous sections we developed the parametric metatheory and prove that it enjoys most of the metaproperties of the classic metatheory. In this section we investigate the relationship between this parametric logical framework and the behavioral properties of CMPs. We begin by recalling a result proved in [CLM11a].

For any
Because the encodings ε and ε preserve the logical implication, a consequence of the fact that CML characterizes stochastic bisimulation is the next theorem.
However, the interrelations between various ε-semantics allow us to prove some stronger results. For this, in what follows, we extend the concept of bisimulation towards a notion of ε-orders that reflect the approximated behaviors. Similar notions have been proposed in literature for less general models. It is the case of the point-wise simulation distance defined in [JS90] for discrete probabilistic systems and similarly in [AHM03,AFS09] for weighted systems, and for general probabilistic systems in [vBW01,D+04].
Recall that for a set C and a relation R, C R denotes the closure of C to R.
Definition 10 (ε-behavioral orders). Given a CMK M = (M, Σ, θ), a relation R ⊆ M × M closed under bisimulation is • an ε-behavioral order whenever m R n, implies that for any C ∈ G M , • an essential ε-behavioral order whenever m R n, implies that for any C ∈ G M , We use ≺ e to denote the largest ε-behavioral order and ≺ + ε to denote the largest essential ε-behavioral order.
Observe that, in the definition of ε-behavioural order we can have θ(n)(C) < θ(m)(C R ), while for essential ε-behavioural order we have always that θ(n)(C) ≥ θ(m)(C R ). Notice also that both ≺ ε and ≺ + ε are not equivalences and that an essential ε-behavioral order is an ε-behavioral order, i.e., ≺ + ε ⊆ ≺ ε . Example 3. Figure 2 shows three discrete processes with initial states m,n and o respectively. Their mutual relationship is easily shown by producing an ε-order. For simplicity, we have not represented the transitions with rate 0. Assuming that s + s = t, we obtain R = {(m, n), (m 1 , n 1 ), (m 2 , n 2 ), (m 4 , n 2 ), (m 3 , n 3 ), (m 5 , n 3 )} ⊆≺ 2ε , i.e., m ≺ 2ε n and the value 2ε is obtained from for C = {m 1 , m 2 , m 4 , n 1 , n 2 }. Observe in this case that m 4 ≺ 2ε n 2 even if the rate of exiting n 2 is smaller than the rate of exiting m 4 . But for this reason we do not have m ≺ + ε n for all ε > 0. Similarly, we obtain m ≺ + ε o for In other words, the rates of m are at most 2ε-smaller than the corresponding rates of n, or larger; and m has at most ε-smaller rates than the corresponding ones of o, but not larger.
Applying Theorem 1 on bisimulation generators, we obatin the following result, which shows the concept of ε-behavioral order generalizes the concept of stochastic bisimulation.
Lemma 5. Any bisimulation relation is an ε-behavioral order for any rational ε ≥ 0. Moreover, if m ∼ n then m ≺ 0 n and n ≺ 0 m.
The next theorem generalizes the theorems 7 and 8 for behavioral orders. In this new context the ε-semantics is the key. Theorem 9 (Logical characterization of ≺ ε ). For arbitrary rational ε ≥ 0, The previous theorem can be further generalized to comprise also the negative formulae. In order to do that, because there is an asymmetry between the behavior of the positive and negative formulae in the ε-semantics, we will need an extra encoding that we define below. This encoding assumes that formulae are in disjunctive normal form (when L r φ are considered atoms).

The pseudometrizable space of processes
In what follows we use ≺ ε to define a canonical distance between CMPs that resemble (and generalize) the well known point-wise distances for particular types of CMPs such as Markov chains. The next result guarantees that between any two systems there is a ≺ ε relation for an ε that is big enough. Lemma 6. For any pair of CMPs m and n there exists a positive rational ε such that m ≺ ε n.
This lemma allows us to define a function  To conclude this section and understand the significance of this distance, we shall take a look at the following example.
Example 4. Consider the CMPs described in Figure 3. We notice that the processes with initial states m and o are quite similar with respect to structure and rate values; the second one has all the transitions ε-bigger than the first one. So a first guess will be that d(m, o) = ε. But this is not the case because the rate of exiting the state m is Consequently, d(m, o) = 3ε. Consider now the CMPs with m and n as initial states and suppose, as before, that s + s = t. We should notice this time that not all the transitions of the first CMP are bigger than the transitions of the second. However, every pair of transitions do not differ with more than ε. Since there are paired transitions that differ with exactly ε value, we obtain that d(m, n) = ε.

Conclusions
In this paper we have introduced a parametric metatheory for Continuous Markovian Logic. The parameter ε of the metatheory encodes an observation error that might appear when we analyze a stochastic system. We define an ε-semantics and an axiomatized ε-proof system and we show that the ε-provability relation is sound and complete with respect to the ε-satisfiability relation. This entire logical framework also allows us to transfer metaproperties between various ε-levels of the metatheory. We prove a series of results regarding the connection between ε-satisfiability and ε + ε -satisfiability and a parameterized deduction theorem that combines ε-provability and ε + ε -provability results.
This classic metalogical framework allows us to give an uniform treatment to all logical properties, including the ones involving negative or logical implication, while avoiding unorthodox logical constructs as the real-valued logics. The framework also supports us in identifying two canonical behavioural orders that extend stochastic bisimulation and organize the space of CMPs. These bisimulation orders are the cornerstones in the definition of a pseudometric on CMPs that measure the behavioral similarity of processes.
The metalogical framework introduced in this paper can be particularized to more specific Markovian models such as the discrete or continuous-time Markov chains. Moreover, the entire development can be adapted to specialize on the probabilistic cases, as the mathematical structure that supports the definition of CMPs is similar to the one that supports the definition of labelled Markov processes in the form of [Pan09].
This paper opens a series of interesting research questions regarding the relationship between εsatisfiability, ε-provability and metric semantics. There are many open questions related to the possibility of defining a pseudometric over the class of logical formulae that shall measure ε-provability; for instance such that the distance between φ and ψ is 0 iff φ and ψ are logical equivalent. On this direction we expect to be able to prove a version of metric completeness that relates the pseudometric space of CMPs to the pseudometric space of logical formulae. The first two authors in collaboration with Prakash Panangaden have already obtained a series of results in this direction [LMP12a,LMP12b]; but these results do not involve the parametric metatheory yet. The hope is that the new metatheoretical perspective introduced in this paper will eventually solve some of the open problems that resisted to the other approaches.