SimSimBisim-Ko.ipynb

{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 시뮬레이션(simulation)과 쌍방시뮬레이션(bisimulation)\n",
    "\n",
    "상태 전이 시스템(state transition system) 중에서 특히 상태 전이가 일어날 때\n",
    "외부에서 관찰가능한 동작의 종류를 라벨(label)을 붙여 놓은 시스템을\n",
    "라벨된 상태 전이 시스템(labeled state transition system)이라 부르기도 하는데, 너무 긴\n",
    "이름이라 라벨된 전이 시스템(labeled transition system)이라 주로 부르며 영문 두문자\n",
    "축약으로는 LTS라고 흔히 표기한다. 이 노트북은 LTS의 형태로 표현된 두 시스템을 비교할\n",
    "때 쓰는 시뮬레이션(simulation)과 쌍방시뮬레이션(bisimulation)이라는 개념을 Haskell로\n",
    "작성된 구체적인 예제를 통해 알아본다.\n",
    "\n",
    "컴퓨터와 관계된 실생활의 대화에서 보통 ***A***가 ***B***를 \"시뮬레이션\"한다고 이야기하는 경우\n",
    "***A***는 ***B***가 할 수 있는 일의 전부는 아니라도 대부분의 일을 따라할 수 있다는 뜻인 경우가 많다.\n",
    "예컨대, 가상머신이나 에뮬레이터 SW가 실제 기계를 시뮬레이션한다는 의미는 실제 기계의 기능 대부분을\n",
    "흉내내지만 하드웨어 가속 등과 같은 특정 기능은 하지 못할 수도 있다.\n",
    "\n",
    "그러나 LTS를 이용한 이론적/수학적인 시스템 설계/모델링에서\n",
    "***A***가***B***를 *시뮬레이션한다*(***A*** *simulates* ***B***)는 의미는\n",
    "***A***는 ***B***가 하는 모든 동작을 그대로 따라할 수 있어야 한다는 뜻이며, 추가로 다른 동작을 더 할 수도 있다.\n",
    "이 때 만일 ***B***도 ***A***를 시뮬레이션한다면***A***와 ***B***는 *상호시뮬레이션한다*(*similar* 또는 *mutual simulation*)고 말한다.\n",
    "즉, 서로가 서로를 시뮬레이션할 수 있다는 말이다."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## LTS 정의\n",
    "시작 상태 하나와 상태들 사이의 라벨된 화살표들로 이루어진 간단한 유한 상태의 LTS를 고려하자.\n",
    "여기서 라벨이 나타내는 바는 상태 전이시 외부에서 관찰할 수 있는 동작(observable action)을 대표한다.\n",
    "어떤 동작을 한 다음에는 다음 상태로 전이, 즉 다음 상태로 옮겨간다.\n",
    "여기서 전이란 현재 상태, 라벨, 다음 상태의 세 가지 요소로 정의된다.\n",
    "\n",
    "하스켈 프로그램으로 두 LTS `systemP`와 `systemQ`를 아래와 같이 정의하였다.\n",
    "관찰 가능한 똑같은 동작 후에 가능한 다음 상태가 여러 개 있을 수 있는 비결정성(non-determinism)을 허용하는 것에 주목하라.\n",
    "이를테면 `systemP`의 `0`번 상태에서 `\"a\"` 라벨된 동작 이후 다음 `1`번 상태로도 갈 수 있고 `2`번 상태로도 갈 수 있다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [],
   "source": [
    "systemP = ( 0, [(0,\"a\",1), (0,\"a\",2), (1,\"b\",3), (2,\"c\",4)] ) -- (startState, edges)\n",
    "systemQ = ( 0, [(0,\"a\",1), (1,\"b\",3), (1,\"c\",4)] )            -- (startState, edges)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "위 두 시스템을 graphviz의 DOT형식으로 [Gravizo](http://www.gravizo.com/)를 통해 그래프로 나타냄으로써 더 직관적으로 시각화하였다.\n",
    "두 시스템을 확실히 구분하기 좋게 방향그래프로 나타낼 때 앞에 글자를 추가했다.\n",
    "예컨대, `systemP`의 2번 상태는 p2로 `systemQ`의 2번 상태는 q2로 표시하였다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [],
   "source": [
    "import IHaskell.Display\n",
    "\n",
    "displayLTS prefix (s,es) = html $ displayLTSsrc prefix (s,es)\n",
    "displayLTSsrc prefix (s,es) = gravizo $ digraphDOT prefix (s,es)\n",
    "gravizo digraphSrc = \"<img src='https://g.gravizo.com/svg?\"++digraphSrc++\"'/>\"\n",
    "digraphDOT prefix (s,es) = \"digraph G { \"\n",
    "  ++ concat [ state p++\" -> \"++state q++\" [label=\"++show a++\"]; \" | (p,a,q)<-es]\n",
    "  ++ \"start -> \"++state s++\"; \"\n",
    "  ++ \"start [shape=none]; \"\n",
    "  ++ \"rankdir = TB; {rank = same; start; \"++state s++\";} \"\n",
    "  ++\"}\"\n",
    "  where state = (prefix++) . show"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><img src='https://g.gravizo.com/svg?digraph G { p0 -> p1 [label=\"a\"]; p0 -> p2 [label=\"a\"]; p1 -> p3 [label=\"b\"]; p2 -> p4 [label=\"c\"]; start -> p0; start [shape=none]; rankdir = TB; {rank = same; start; p0;} }'/>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "displayLTS \"p\" systemP"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><img src='https://g.gravizo.com/svg?digraph G { q0 -> q1 [label=\"a\"]; q1 -> q3 [label=\"b\"]; q1 -> q4 [label=\"c\"]; start -> q0; start [shape=none]; rankdir = TB; {rank = same; start; q0;} }'/>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "displayLTS \"q\" systemQ"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 시뮬레이션(simulation)의 정의\n",
    "$\\mathcal{R}$은 이항관계로서 \n",
    "$q_0$로 시작하는 라벨된 전이 시스템 $Q$와 $p_0$로 시작하는 라벨된 시스템 $P$의 상태를 관련짓는다.\n",
    "\n",
    "다음 두 조건을 만족하는 관계 $\\mathcal{R}$이 정의될 때 $Q$가 $P$를 시뮬레이션한다.\n",
    " * $p_0 \\mathcal{R}\\,q_0$\n",
    " * $\\forall a, \\forall p_i,~ p \\xrightarrow{~a~} p_i, ~ \\exists q_j,~ q \\xrightarrow{~a~} q_j\\;$ such that $\\;p_i\\mathcal{R}\\,q_j$\n",
    "\n",
    "이러한 관계 $\\mathcal{R}$을 시뮬레이션 관계라고 부른다.\n",
    "또한 구체적으로 상태를 지목해 $q_j$가 $p_i$를 시뮬레이션한다고 표현할 수 있으며 이를 $p_i\\mathcal{R}\\,q_j$로 표기한다.\n",
    "이 관계는 원순서(preorder)이므로 $p_i \\preceq q_j$와 같은 방식으로 시뮬레이션 관계를 표기하는 경우도 종종 있다.\n",
    "\n",
    "관계 $\\mathcal{R}$을 순서쌍의 집합으로 계산하는 대신\n",
    "아래와 같이 하스켈로는 진리값 결과를 갖는 이항함수(`sim`)로 구현하였다.\n",
    "이 함수는 순서쌍이 관계집합에 속하는지 즉 $(p_j,q_i)\\in\\mathcal{R}$를 검사하는 것에 해당한다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [],
   "source": [
    "-- test whether  sysP starting from p0   simulates  sysQ starting from q0\n",
    "simulates sysQ@(q0,esQ) sysP@(p0,esP) = sim p0 q0\n",
    "  where\n",
    "  sim p q = and [or [sim p1 q1 | (q',b,q1) <- esQ, q==q', a==b] -- (or  ...) exists a mathcing step from q\n",
    "                               | (p',a,p1) <- esP, p==p']       -- (and ...) for each step starting from p"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "상호시뮬레이션(`similar`)은 서로가 서로를 시뮬레이션 할 수 있는지로 정의한다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [],
   "source": [
    "similar sysP sysQ = simulates sysP sysQ && simulates sysQ sysP"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`systemQ`는 `systemP`를 시뮬레이션하지만 그 반대는 아니다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 7,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "systemP `simulates` systemQ\n",
    "systemQ `simulates` systemP\n",
    "systemP `similar` systemQ"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`systemQ`의 $q_1$ 상태에서는 `systemP`의 $p_1$ 상태에서 할 수 있는 일을 모두 따라할 수 있고 $p_2$ 상태에서 할 수 있는 일도 모두 따라할 수 있다.\n",
    "\n",
    "그러나 `systemP`의 $p_1$ 상태나 $p_2$ 상태에서는 `systemQ`의 $q_1$ 상태에서 할 수 있는 일을 모두 따라할 수 없다.\n",
    "$p_1$에서는 라벨 $c$ 동작을 따라할 수 없고 $p_2$에서는 라벨 $b$ 동작을 따라할 수 없음을 관찰할 수 있을 것이다."
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 상호 시뮬레이션 (mutual simulation)\n",
    "`systemP`에 전이 $p_2 \\xrightarrow{~b~} p_3$를 추가한 `systemP'`을 정의하자."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/html": [
       "<style>/* Styles used for the Hoogle display in the pager */\n",
       ".hoogle-doc {\n",
       "display: block;\n",
       "padding-bottom: 1.3em;\n",
       "padding-left: 0.4em;\n",
       "}\n",
       ".hoogle-code {\n",
       "display: block;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "}\n",
       ".hoogle-text {\n",
       "display: block;\n",
       "}\n",
       ".hoogle-name {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-head {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-sub {\n",
       "display: block;\n",
       "margin-left: 0.4em;\n",
       "}\n",
       ".hoogle-package {\n",
       "font-weight: bold;\n",
       "font-style: italic;\n",
       "}\n",
       ".hoogle-module {\n",
       "font-weight: bold;\n",
       "}\n",
       ".hoogle-class {\n",
       "font-weight: bold;\n",
       "}\n",
       ".get-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "white-space: pre-wrap;\n",
       "}\n",
       ".show-type {\n",
       "color: green;\n",
       "font-weight: bold;\n",
       "font-family: monospace;\n",
       "margin-left: 1em;\n",
       "}\n",
       ".mono {\n",
       "font-family: monospace;\n",
       "display: block;\n",
       "}\n",
       ".err-msg {\n",
       "color: red;\n",
       "font-style: italic;\n",
       "font-family: monospace;\n",
       "white-space: pre;\n",
       "display: block;\n",
       "}\n",
       "#unshowable {\n",
       "color: red;\n",
       "font-weight: bold;\n",
       "}\n",
       ".err-msg.in.collapse {\n",
       "padding-top: 0.7em;\n",
       "}\n",
       ".highlight-code {\n",
       "white-space: pre;\n",
       "font-family: monospace;\n",
       "}\n",
       ".suggestion-warning { \n",
       "font-weight: bold;\n",
       "color: rgb(200, 130, 0);\n",
       "}\n",
       ".suggestion-error { \n",
       "font-weight: bold;\n",
       "color: red;\n",
       "}\n",
       ".suggestion-name {\n",
       "font-weight: bold;\n",
       "}\n",
       "</style><img src='https://g.gravizo.com/svg?digraph G { p0 -> p1 [label=\"a\"]; p0 -> p2 [label=\"a\"]; p1 -> p3 [label=\"b\"]; p2 -> p3 [label=\"b\"]; p2 -> p4 [label=\"c\"]; start -> p0; start [shape=none]; rankdir = TB; {rank = same; start; p0;} }'/>"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "systemP' = (0, [(0,\"a\",1), (0,\"a\",2), (1,\"b\",3), (2,\"b\",3), (2,\"c\",4)]) -- (startState, edges)\n",
    "\n",
    "displayLTS \"p\" systemP'"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "새로 정의한 `systemP'`와 앞서 정의한  `systemQ`가 상호시뮬레이션함을 관찰해 보자.\n",
    "즉, `systemP'`가 `systemQ`를 시뮬레이션할 수 있을 뿐 아니라 `systemQ`도 `systemP'`을 시뮬레이션 할 수 있다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "systemP' `simulates` systemQ\n",
    "systemQ  `simulates` systemP'\n",
    "systemP' `similar` systemQ"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 쌍방시뮬레이션(bisimulation)의 정의\n",
    "$\\mathcal{R}$은 이항관계로서 \n",
    "$p_0$로 시작하는 라벨된 전이 시스템 $P$와 $q_0$로 시작하는 라벨된 시스템 $Q$의 상태를 관련짓는다.\n",
    "\n",
    "다음 세 조건을 만족하는 관계 $\\mathcal{R}$이 정의될 때 $P$와 $Q$는 쌍방시뮬레이션 관계에 있다고 한다.\n",
    " * $p_0 \\mathcal{R}\\,q_0$\n",
    " * $\\forall a, \\forall p_i,~ p \\xrightarrow{~a~} p_i, ~ \\exists q_j,~ q \\xrightarrow{~a~} q_j\\;$ such that $\\;p_i\\mathcal{R}\\,q_j$\n",
    " * $\\forall a, \\forall q_j,~ q \\xrightarrow{~a~} q_j, ~ \\exists p_i,~ p \\xrightarrow{~a~} p_i\\;$ such that $\\;p_i\\mathcal{R}\\,q_j$ \n",
    "\n",
    "이러한 관계 $\\mathcal{R}$을 쌍방시뮬레이션 관계라고 한다.\n",
    "또한 구체적으로 상태를 지목해 $p_i$와 $q_j$가 쌍방시뮬레이션 관계라고 표현할 수 있으며 이를 $p_i\\mathcal{R}\\,q_j$로 표기한다.\n",
    "이 관계는 동치관계이므로 $p_i \\sim q_j$와 같은 방식으로 쌍방시뮬레이션을 표기하는 경우가 많다.\n",
    "\n",
    "관계 $\\mathcal{R}$을 순서쌍의 집합으로 계산하는 대신\n",
    "아래와 같이 하스켈로는 진리값 결과를 갖는 이항함수(`bisim`)로 구현하였다.\n",
    "이 함수는 순서쌍이 관계집합에 속하는지 즉 $(p_i,q_j)\\in\\mathcal{R}$를 검사하는 것에 해당한다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [],
   "source": [
    "-- test whether  sysP starting from p0   is bisimilar to  sysQ starting from q0\n",
    "bisimilar sysP@(p0,esP) sysQ@(q0,esQ) = bisim p0 q0\n",
    "  where\n",
    "  bisim p q = and [or [bisim p1 q1 | (q',b,q1) <- esQ, q==q', a==b]\n",
    "                                   | (p',a,p1) <- esP, p==p']\n",
    "           && and [or [bisim p1 q1 | (p',a,p1) <- esP, p==p', b==a]\n",
    "                                   | (q',b,q1) <- esQ, q==q']"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "similar    systemP  systemQ\n",
    "bisimilar  systemP  systemQ -- obviously false, was not even simialr"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    },
    {
     "data": {
      "text/plain": [
       "False"
      ]
     },
     "metadata": {},
     "output_type": "display_data"
    }
   ],
   "source": [
    "similar    systemP' systemQ\n",
    "bisimilar  systemP' systemQ -- oh! similar but not bisimilar ?!?!"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 방금 무슨 일이 일어났지?"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "위에서 쌍방시뮬레이션이 실패하는 이유는 바로 여기에 있다.\n",
    " 1. 첫번째로 `systemP'`가 앞선 걸음으로 $p_0 \\xrightarrow{~a~} p_1$ 동작을 한다.\n",
    "      - 그러면 `systemQ` 입장에서 이를 따라하는 걸음을 취하라면 $q_0 \\xrightarrow{~a~} q_1$ 동작 말고는 선택의 여지가 없다.\n",
    " 1. 그 다음 두번째에는 `systemQ`가 가 앞선 걸음 $q_1 \\xrightarrow{~c~} q_4$ 동작을 취한다. \n",
    "      - 이제 `systemP'`는 이를 **따라하는 걸음을 내딛을 수가 없다**. 왜냐하면 $p_1$에서 라벨 $c$ 동작을 할 수 없기 때문이다.\n",
    "\n",
    "상호시뮬레이션을 검사하는 함수 `similar`를 실행할 때는 위와 같은 쌍방시뮬레이션 단계들이 고려되지 않는다.\n",
    "왜냐하면 상호시뮬레이션에서는 앞선 걸음과 따라하는 걸음을 하는 역할이 두 번의 각각의 시뮬레이션 검사를 할 때 고정되어 있기 때문이다.\n",
    "한쪽이 앞선 걸음을 하면 다른쪽은 그를 따라하는 걸음만 하면 된다. 반면 쌍방시뮬레이션에서는 양쪽 모두가 각각 앞선 걸음과 따라하는 걸음의 역할을 하는 경우를 쌍방시뮬레이션의 매 단계마다 고려해야 한다. 그렇기에 쌍방시뮬레이션(bisimulation)은 상호시뮬레이션(mutual simulation)보다 더 강력한 (또는, 더 섬세하게 구분 가능한) 동치관계라 할 수 있다."
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {},
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Haskell",
   "language": "haskell",
   "name": "haskell"
  },
  "language_info": {
   "codemirror_mode": "ihaskell",
   "file_extension": ".hs",
   "name": "haskell",
   "pygments_lexer": "Haskell",
   "version": "8.6.5"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 4
}