Markovian Logics: The Metric Space of Logical Formulas. The Bulletin of Symbolic Logic, the meeting report of Logic Colloquium 2011

A central questions in the field of probabilistic and Markovian systems is “when do two systems behave similarly up to some observational error?”. Probabilistic and stochastic bisimulations relates models with identical behaviours and are characterized by multimodal logics with operators indexed with transition probabilities or rates [3, 4, 5]. In spite of their elegant theories, these concepts are too strict for applications where the parameters of a model are approximated. Thus, the interest shifts from identical to similar behaviours and the bisimulations are replaced by a class of pseudometrics [5]: two processes are at distance zero iff they are bisimilar and are close when they differ by a small amount in their quantitative behaviours. These pseudometrics are defined on top of the logics that characterize bisimulations: the satisfiability relation P φ (for a process P ∈ P and a logical formula φ ∈ L) is approximated by a function d: P×L → [0, 1] such that d(P, φ) = 0 iff P φ. d induces a distance D on processes by D(P, P ′) = sup{|d(P, φ)−d(P ′, φ)|, φ ∈ L} and similarly, a pseudometric δ on formulas by δ(φ, ψ) = sup{|d(P, φ)−d(P,ψ)|, P ∈ P. In the context of complete axiomatizations for the probabilistic and stochastic logics [1, 2, 3, 6], one can prove that δ is a measur