wip

ACV-abstract-2026/references.bib

@@ -9,6 +9,14 @@
 @STRING{lnm	= "LNM" }
 @STRING{springer= "Springer" }
 
+@Article{         Staton11,
+  author        = {Sam Staton},
+  title         = {Relating coalgebraic notions of bisimulation},
+  journal       = {Log.\ Methods Comput.\ Sci.},
+  year          = {2011},
+  volume        = {7}
+}
+
 @Proceedings{	  2015IEEE,
   title		= {2015 {IEEE} Symposium on Security and Privacy, {SP} 2015,
 		  San Jose, CA, USA, May 17-21, 2015},

ACV-abstract-2026/sym-sim.tex

@@ -3,7 +3,7 @@
 \PassOptionsToPackage{nosumlimits,nonamelimits}{amsmath}
 \PassOptionsToPackage{colorlinks,linkcolor={blue},citecolor={blue},urlcolor={red},breaklinks=true,final}{hyperref}
 
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, numberwithinsect,final]{lipics-v2021}
+\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate, final]{lipics-v2021}
 \bibliographystyle{plainurl} % the mandatory bibstyle
 
 \sloppy
@@ -72,21 +72,20 @@
 \newcommand{\klstar}{\sharp}  			%% Kleisli star
 \newcommand{\relar}{\mathbf{R}}
 
-\title{Soundness and Completeness of Symmetric Relators} %TODO Please add
+\title{Coalgebraic Notions of Simulation, Bisimulation and Relators} %TODO Please add
 %Or: It is expected from a symmetric simulation to be a bisimulation
-\titlerunning{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly}
+%\titlerunning{From Abstract Higher-Order GSOS to Abstract Big-Step Semantics, Abstractly}
 
-\author{Sergey Goncharov}{University of Birmingham, UK}{s.goncharov@bham.ac.uk}{https://orcid.org/0000-0001-6924-8766}{}
 \author{Pouya Partow}{University of Birmingham, UK}{p.partow@bham.ac.uk}{https://orcid.org/0009-0003-9652-9469}{}
+\author{Sergey Goncharov}{University of Birmingham, UK}{s.goncharov@bham.ac.uk}{https://orcid.org/0000-0001-6924-8766}{}
 
-
+%\authorrunning{J. Open Access and J.\,R. Public} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
-\authorrunning{J. Open Access and J.\,R. Public} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
 
 \Copyright{Jane Open Access and Joan R. Public} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
 
 %\ccsdesc[100]{\textcolor{red}{Replace ccsdesc macro with valid one}} %TODO mandatory: Please choose ACM 2012 classifications from https://dl.acm.org/ccs/ccs_flat.cfm 
 
-\keywords{Operational semantics, Higher-order GSOS, Extended combinatory logic}
+%\keywords{Operational semantics, Higher-order GSOS, Extended combinatory logic}
 
 \category{} %optional, e.g. invited paper
 
@@ -123,6 +122,8 @@
 \def\subjclassHeading{}
 \makeatletter
 \def\@ccsdescString{\erule\vspace{-5ex}}
+\def\keywordsHeading{}
+\def\@keywords{\relax}
 \makeatother
 
 
@@ -133,12 +134,6 @@
 
 \maketitle
 
-%TODO mandatory: add short abstract of the document
-\begin{abstract}
- 
-%One remarkable aspect of our approach is its potential for implementation in functional programming languages and proof assistants, 
-%to atomate SOS specification transformations and reasoning about them.
-\end{abstract}
 
 
 
@@ -179,6 +174,59 @@
 
 %There exist various notions of (bi)simulation in the literature. For some of them, it is expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion. A more advanced example is in Howe's method. Howe's method is used to prove that applicative bisimilarity is a congruence. It is done by applying Howe closure on bisimilarity, and then proving that the given relation is a bisimulation. Howe closure of bisimilarity includes it and preserves its symmetry. More importantly, Howe closure of bisimilarity is a congruence. Given the non-symmetric nature of Howe closure, it is more common to prove that applying Howe closure on the bisimilarity, gives a simulation, and then we have the rest. But getting to bisimulation from having a symmetric simulation is a step that we believe needs to be taken with care, and we discuss here.
 
+
+\bigskip
+
+Notions of simulation and bisimulation play a central role in the theory of transition 
+systems and in program semantics. Bisimulation is a certain canonical notion of program 
+(or system) equivalence, which can be formulated in different equivalent ways in 
+base cases, while these ways need not remain equivalent under further generalizations. 
+This is acknowledged and investigated in the literature (see e.g.\ \cite{Staton11}).
+Contrastingly, \emph{simulation} is a non-canonical notion of program in-equivalence 
+(or approximation), subject to the same issue, but much less explored in this case. 
+Consider the following baseline example. 
+%
+\begin{example}[Kripke Frame, Simulation, Bisimulation] A Kripke frame consists 
+of a set $W$ and a function $c\c W\to\PSet W$ (equivalently: relation $r\subseteq W\times W$).
+
+Simulation on $(W, C)$ is such a relation $r\subseteq W\times W$ that $(x,y)\in r$ 
+entails: for all $x'\in c(x)$ there is $y'\in c(y)$, such that $(x',y')\in r$.
+Such a relation is a bisimulation if additionally $(x,y)\in r$ 
+entails: for all $y'\in c(y)$ there is $x'\in c(x)$, such that $(x',y')\in r$.
+
+Thus, $r$ is a bisimulation iff both $r$ and its inverse $r^\circ$ are simulations.
+\end{example}
+%
+These setting can be varied at least in two ways: 
+%
+\begin{itemize}
+  \item The powerset functor $\PSet$ can be replaced by another endofunctor $F\c\Set\to\Set$
+  (to model systems with input, output, probability, nontermination, etc.)
+  \item A different underlying category $\BC$ can be used in place of $\Set$ (e.g.\
+  nominal sets, to model systems with name management). 
+\end{itemize}
+%
+A convenient way to work with simulations and bisimulations is via the notion of 
+\emph{relator}. 
+
+\begin{definition}[Relators, Simulation, Bisimulation]
+Given a set functor $F\c\Set\to\Set$, an \emph{$F$-relator} is a monotone map $\relar$
+sending a relation $r\subseteq X\times Y$ to a relation $\relar r\subseteq FX\times FY$.
+A relator $\relar$ is \emph{symmetric} if $\relar(r^\op)=(\relar r)^\op$, and
+\emph{normal} if $\relar 1_X=1_{FX}$.
+
+A relation $r\subseteq X\times Y$ is an \emph{$\relar$-simulation} from an
+$F$-coalgebra $(X,\alpha)$ to $(Y,\beta)$ if
+\[
+  r \;\subseteq\; \beta^\op\comp\relar r\comp\alpha,
+\]
+i.e.\ $x\mathrel{r}y$ implies $\alpha(x)\mathrel{\relar r}\beta(y)$.
+The greatest $\relar$-simulation from $(X,\alpha)$ to $(Y,\beta)$ (which exists by
+Knaster-Tarski) is \emph{$\relar$-similarity}. When $\relar$ is symmetric,
+$\relar$-simulations are called \emph{$\relar$-bisimulations} and $\relar$-similarity
+is called \emph{$\relar$-bisimilarity}.
+\end{definition}
+
 There exist various notions of (bi)simulation in the literature. It is usually expected from a symmetric simulation to be a bisimulation. It is true for the most traditionally known notion, but such conclusion must be made with care. We describe a scenario, in which we have a proof that a symmetric relation is a simulation, but the proof does not serve as a proof for the relation to be a bisimulation. 
 We take the Aczel-Mendler simulation\cite{Dubut25}. Given a partial order over a functor $F\c\BC\to\BC$, a relation $r$ on $X$ is a simulation on a coalgebra $(X,\alpha)$ iff there exists a coalgebra $(R,\sigma)$ called \emph{witness} that laxly commutes in the following diagram:
 \begin{equation}\label{eq:diag-lax-sim}
@@ -210,9 +258,10 @@ In this scenario, $\sigma$ is a witness for $r$ to be a simulation, but it is no
 
 Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the definition by setting $\BC$ to be a regular category, and changing the span $(FR,Fp_1,Fp_2)$ in~\eqref{eq:diag-lax-sim} with the span $((Fr)^\dagger,(Fp_1)^\dagger,(Fp_2)^\dagger)$, where $(Fr)^\dagger$ is the image of $\brks{Fp_1,Fp_2}$, and $\brks{(Fp_1)^\dagger,(Fp_2)^\dagger}\c(FR)^\dagger\to FX\times FX$ is monic, so $(Fr)^\dagger$ is a relation. By the symmetry of $r$ there exists $s\c r\to r$ that we call \emph{swap}, where $p_1\comp s=p_2$ and $p_2\comp s=p_1$. The necessary and sufficient condition for $\sigma$ to be a witness for $r$ to be a bisimulation is that
 \begin{gather}\label{eq:nec-suf-sim}
-	\sigma\comp s=(Fs)^\dagger\comp\sigma
+	\sigma\comp s=(Fs)^\dagger\comp\sigma,
 \end{gather}
- , i.e., $s$ is a $F$-coalgebra morphism from $\sigma$ to itself. Nevertheless, still we have the following example of the $\sigma\c r\to(Fr)^\dagger$ that is a witness for $r$ to be a simulation over $(X,\alpha)$, but it is not a witness for $r$ to be a bisimulation. Keeping the setting of the previous example, we modify $\sigma$ as follows:
+%
+i.e., $s$ is a $F$-coalgebra morphism from $\sigma$ to itself. Nevertheless, still we have the following example of the $\sigma\c r\to(Fr)^\dagger$ that is a witness for $r$ to be a simulation over $(X,\alpha)$, but it is not a witness for $r$ to be a bisimulation. Keeping the setting of the previous example, we modify $\sigma$ as follows:
  \begin{gather*}
  	\sigma(w)=
  	\begin{cases} 
@@ -223,8 +272,9 @@ Inspired by Hermida-Jacobs bisimulation\cite{HermidaJacobs98} we modify the defi
  $\sigma$ is a witness for $r$ to be a simulation since for every $w\in r$ we have $\alpha(p_1(w))\subseteq((\mathcal{P}p_1)^\dagger(\sigma(w)))=X$. Also, for every $w\in r$, $((\mathcal{P}p_2)^\dagger(\sigma(w)))\subseteq\alpha(p_2(w))=X$. But it is not a bisimulation, since $\alpha(p_2(1,3))=\alpha(3)=X\neq(\mathcal{P}p_2)^\dagger(\sigma(1,3))=X\setminus\{2\}$.
 It worth mentioning that $\sigma$ does not satisfy~\eqref{eq:nec-suf-sim}. But still we do not know if having such $\sigma$ can give us a witness that satisfies~\eqref{eq:nec-suf-sim} or guarantees the existence of such witness.
 
-There is a solution for this problem, if we change the context. If we take our category to be $\Set$, we can talk about a kind of well-studied maps named \emph{relator}. For a set functor $F$, a relator $\relar$ takes a relation $r\subseteq X\times Y$ to another relation $\relar r\subseteq FX\times FY$. A relator is monotone with respect to inclusion. For example, in our alternative for Aczel-Mendler simulation, for every set functor $F$, the map that takes a relation $r$ to $(Fr)^\dagger$ is a relator.  We show the reverse of a relation $r$ with $r^\op$, and composition of $r$ with another relation $t$ with $t\comp r$. A relation $r\subseteq X\times Y$ is called $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ iff $r\subseteq \beta\comp\relar r\comp\alpha^\op$. Additionally, a relator is called symmetric iff $\relar (r^\op)=(\relar r)^\op$, and a $\relar$-simulation for a symmetric $\relar$ is called a $\relar$-bisimulation that resembles~\eqref{eq:nec-suf-sim}. $\relar$-similarity and $\relar$-bisimilarity are the greatest $\relar$-simulation and $\relar$-bisimulation, respectively. We call a relator $\relar$ sound iff $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is included in the behavioural equivalence from $(X,\alpha)$ to $(Y,\beta)$, and we call it complete iff the behavioural equivalence is included in the $\relar$-similarity. 
+There is a solution for this problem, if we change the context. If we take our category to be $\Set$, we can talk about a kind of well-studied maps named \emph{relator}. For a set functor $F$, a relator $\relar$ takes a relation $r\subseteq X\times Y$ to another relation $\relar r\subseteq FX\times FY$. A relator is monotone with respect to inclusion. For example, in our alternative for Aczel-Mendler simulation, for every set functor $F$, the map that takes a relation $r$ to $(Fr)^\dagger$ is a relator.  We show the reverse of a relation $r$ with $r^\op$, and composition of $r$ with another relation $t$ with $t\comp r$. A relation $r\subseteq X\times Y$ is called $\relar$-simulation from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ iff $r\subseteq \beta^\op\comp\relar r\comp\alpha$. Additionally, a relator is called symmetric iff $\relar (r^\op)=(\relar r)^\op$, and a $\relar$-simulation for a symmetric $\relar$ is called a $\relar$-bisimulation that resembles~\eqref{eq:nec-suf-sim}. $\relar$-similarity and $\relar$-bisimilarity are the greatest $\relar$-simulation and $\relar$-bisimulation, respectively. We call a relator $\relar$ sound iff $\relar$-similarity from a coalgebra $(X,\alpha)$ to a coalgebra $(Y,\beta)$ is included in the behavioural equivalence from $(X,\alpha)$ to $(Y,\beta)$, and we call it complete iff the behavioural equivalence is included in the $\relar$-similarity. 
-\newpage
+
+
 \bibliography{references}