Correspondences.thy

(*<*)
theory Correspondences
  imports 
    Pure
begin
(*>*)

chapter \<open>Characterizing Equivalences \label{chap:CharEq}\<close>

text \<open>In this section, we establish the correspondence between characterizations based on price coordinates and modal-logical characterizations. 
For an in-depth explanation of the equivalences and there respective place in the linear-time--branching-time spectrum, we refer to \cite{GLABBEEK20013}.

Our aim is to demonstrate that for each equivalence X within the linear-time--branching-time spectrum, the modal-logical characterization $\mathcal{O}_X$, derived from \cite{GLABBEEK20013}, captures the same notion of equivalence as the price characterization $\mathcal{O}_{e_{X}}$ with price coordinate $e_X$ as in Figure \ref{fig:1_1}. For most equivalences, these characterizations do not encompass the same set of formulas. Instead, we use induction in both directions to construct equivalent formulas for each formula in the respective set.
To illustrate the structure of the proofs, we present a comprehensive proof for the correspondence of failure traces \ref{sec:FT}. The underlying concepts of the proof are applicable to the other propositions, given that their proofs work similarly. For the other propositions, we provide the intuition and outline proof sketches.\<close>

(*<*)
end
(*>*)