development

background.tex

@@ -58,7 +58,7 @@
       Let \(\gamma = {\left\{C_i\right\}}_{i\in [0, n]}\) a context sequence. Given a positive integer \(k \leq n\), let \(\gamma^{k} \defeq {\left\{C_{i+k}\right\}}_{i\in [0, n-k]}\).
     \end{definition}
 
-    \begin{subsection}{Example: A binary counter}
+    \begin{subsection}{Example: A binary counter}\label{binary_counter}
       A reaction system can act as a cyclic n-bit counter in which external signals trigger increment or decrement operations. To build the counter, let \(n > 0\) be an integer and define the background set as \( \{p_0, p_1, \ldots, p_{n-1}\} \cup \{ dec, inc\} \).
 
       Five sets of reactions describe a binary counter-like behavior:
@@ -79,6 +79,15 @@
       \(C_0 = \{p1, p3\}, C_1 = \emptyset, C_2 = \{inc\}, C_3 = \{inc\}, C_4 = \{dec\}, C_5 = \{dec, inc\}\). This gives the result sequence \(\delta = \emptyset.\{p1, p3\}.\{p1, p3\}.\{p0, p1, p3\}.\{p2, p3\}.\{p0, p1, p3\}.\emptyset\) and state sequence \(\tau = \{p1, p3\}.\{p1, p3\}.\{p1, p3, inc\}.\{p0, p1, p3, inc\}.\{p2, p3, dec\}.\{p0, p1, p3, dec, inc\}.\emptyset\) that in binary representation is \(\{1010\}.\{1010\}.\{1010\}.\{1011\}.\{1100\}.\{1011\}.\{0000\}\) by ignoring \(inc\) and \(dec\).
     \end{subsection}
 
+    \begin{subsection}{Simple loops}
+      The result sequence of a RS, generated by applying the reactions, can be different from \(\emptyset\) for an infinite number of results. But if two results are the same, also the following result will be the same. This implies the existence of a loop of states. To identify a loop one can simply truncate the trace at position \(n\) and search for the result in position \(n+1\) in the truncated trace.
+
+      If the entities provided by the context are not constant, the behavior might not be as easily described. By restricting only on a constant set provided by the context, we can be sure that the computation will find a loop.
+
+      These loops are called \textit{lollipops}.
+
+      For example by providing the set \(\{inc\}\) as the context at each step of the system from Example\ \ref{binary_counter}, we obtain the loop: \(\{p1, p3\}.\{p0, p1, p3\}.\{p3, p2\}.\{p0, p3, p2\}.\{p1, p3, p2\}.\{p0, p1, p3, p2\}.\{\}.\{p0\}.\{p1\}.\{p0, p1\}.\{p2\}.\{p0, p2\}.\{p1, p2\}.\{p0, p1, p2\}.\{p3\}.\{p0, p3\}\).
+    \end{subsection}
   \end{section}
 
   \begin{section}{SOS rules for reaction systems}\label{SOS_rules_section}
@@ -249,7 +258,7 @@
       In general one can apply a minimization process to both standard and Positive RS and derive a simplified version of the original system with fewer reactions.
     \end{subsection}
 
-    \begin{subsection}{Slicing}
+    \begin{subsection}{Slicing}\label{slicing}
       In the context of programming, dynamic slicing is a technique that helps a user to debug a program by simplifying a partial execution trace, by pruning parts which are irrelevant and highlighting parts of the program wich are responsible for the production of an error.
       In the case of RSs, the goal is to highlight how a subset of the elements in a state were originated. This include the reactants and reactions that were responsible for producing them.
 
@@ -283,7 +292,7 @@
     \end{subsection}
   \end{section}
 
-  \begin{section}{Bisimulation}
+  \begin{section}{Bisimulation}\label{bisimulation}
     Given two distinct RS processes, the natural question to ask would be if their simulation is the same, or at least behaves the same. Bisimulation is one such relation, defined in terms of coinductive games, of fixed point theory and of logic.
     Bisimulation equivalence aims to identify transitions systems with the same branching structure, and wich thus can simulate each other in a stepwise manner.