Answers.Body: <p><strong>This is how I see it:</strong></p>
  <p>The state that a purely reactive agent is reacting to is, in fact, a subset of the set of all possible runs that end with a state. So in theory, <em>E</em> (some state) is a subset of <em>R</em> (finite set of all possible runs with a state as the last element). Standard and purely reactive agents are similar in the sense that the agents' purpose is to commit an action given some condition. It is entirely possible that a standard agent might be dealing with a run which encompasses only one element. Therefore, this would imply that for a discrete event in time, the standard agent's behaviour would be equivalent to a purely reactive agent, right? or am I completely off the rails?</p>
  <p>Sorry for not using the required symbols, I'm new here and am getting used to the styling :D</p>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-01-20T13:09:51.223Z
Answers.Text: I think there needs to be a better definition for individual states. In your case and my case, we are implying that *E* is a subset of *R*, however, in that case, we are implying a whole set of elements, as opposed to any individual element. A whole run may not have all the states in the set *E*, however it would require at least **one state**.  Therefore any particular element in the set *E* is a subset of *R*, and therefore, for every possible purely reactive agent that is reacting to some state *e* ∈ *E*, there is a behaviourally equivalent standard agent
Answers.UserDisplayName: Jonathan Cauchi
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2021-01-20T12:59:54.857Z
Answers.LastActivityDate: 2021-01-20T12:59:54.857Z
Answers.UserDisplayName: Jonathan Cauchi
Answers.Body: <p>I recommend you to look into the literature about <em>simulation</em> and <em>bisimulation</em> in Automata Theory and its applications to model checking (where you want to make quite regularly proofs of "behavioural equivalence"). One article that discusses this in the context of a technique for model checking known as <em>"Abstraction and Abstraction Refinement"</em> is</p>
  
  <pre><code>Abstraction and Abstraction Refinement
  Dennis Dams and Orna Grumberg
  In Springer's Handbook of Model Checking, 2018, Chapter 13, pages 385-420
  </code></pre>
  
  <p>A good (I use it regularly) book that covers behavioural equivalence for a wide variety of automata is </p>
  
  <pre><code>Verification and Control of Hybrid Systems: A Symbolic Approach
  Paulo Tabuada
  Springer, 2009
  </code></pre>
  
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-03-22T08:54:48.297Z
Answers.Text: Thanks for the suggested readings. Will definitely take a look
Answers.UserDisplayName: aidar_ms
Answers.ContentLicense: CC BY-SA 4.0
Answers.CreationDate: 2020-02-19T10:02:54.663Z
Answers.LastActivityDate: 2020-02-19T10:02:54.663Z
Answers.UserDisplayName: Miquel Ramirez
Body: <p>It kind of makes sense intuitively but I'm not sure about a formal proof. I'll start with briefly listing definitions from <strong>Intro to Multiagent systems, Wooldridge, 2002</strong> and then give you my reasoning attempts thus far.</p>
  
  <p><span class="math-container">$E$</span> is a finite set of discrete, instantaneous states, <span class="math-container">$E=(e, e',...)$</span>. <span class="math-container">$Ac$</span> is a repertoire of possible actions (also finite) available to an agent, which transform the environment, <span class="math-container">$Ac=(\alpha, \alpha', ...)$</span>. A run is a sequence of interleaved environment states and actions, <span class="math-container">$r=(e_0, \alpha_0, e_1, \alpha_1,..., \alpha_{u-1}, e_u)$</span>, set of all such possible finite sequences (over <span class="math-container">$E$</span> and <span class="math-container">$Ac$</span>) is <span class="math-container">$R$</span>, <span class="math-container">$R^E$</span> is a subset of <span class="math-container">$R$</span> containing the runs that end with an env. state.</p>
  
  <p>Purely reactive agent is modeled as: <span class="math-container">$Ag_{pure}: E\mapsto Ac$</span>, a standard agent is modeled as <span class="math-container">$Ag_{std}: R^E\mapsto Ac$</span>.</p>
  
  <p>So, if <span class="math-container">$R^E$</span> is a sequence of agent's actions and environment states, than it just makes sense that <span class="math-container">$E\subset R^E$</span>. Hence, <span class="math-container">$Ag_{std}$</span> can map to every action to which <span class="math-container">$Ag_{pure}$</span> can. And behavioral equivalence with respect to environment <span class="math-container">$Env$</span> is defined as <span class="math-container">$R(Env, Ag_{1}) = R(Env, Ag_{2})$</span>; where <span class="math-container">$Env=\langle E,e_{0},t \rangle$</span>, <span class="math-container">$e_{0}$</span> - initial environment state, <span class="math-container">$t$</span> - transformation function (definition irrelevant for now).</p>
  
  <p>Finally, if <span class="math-container">$Ag_{pure}: E\mapsto Ac$</span> <strong>and</strong> <span class="math-container">$Ag_{std}: R^E\mapsto Ac$</span>, <strong>and</strong> <span class="math-container">$E\subset R^E$</span>, we can say that <span class="math-container">$R(Env,Ag_{pure}) = R(Env, Ag_{std})$</span> (might be too bold of an assumption). Hence, every purely reactive agent has behaviorally equivalent standard agent. The opposite might not be true, since <span class="math-container">$E\subset R^E$</span> means that all elements of <span class="math-container">$E$</span> belong to <span class="math-container">$R^E$</span>, while not all elements <span class="math-container">$R^E$</span> belong to <span class="math-container">$E$</span>.</p>
  
  <p>It's a textbook problem, but I couldn't find an answer key to check my solution. If anyone has formally (and perhaps mathematically) proven this before, can you post your feedback, thoughts, proofs in the comments? For instance, set of mathematical steps to infer <span class="math-container">$E\subset R^E$</span> from their definitions: <span class="math-container">$E=(e_{0}, e_{1},..., e_{u})$</span> and <span class="math-container">$R^E$</span> is "<em>all agent runs that end with an environment state</em>" (no formal equation found) is not clear to me.</p>
  
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-02-19T01:07:36.300Z
Comments.Text: Hi and welcome to AI SE. You say "if $R^E$ is a sequence of agent's actions and environment states, than it just makes sense that $E \subset R^E$", but I would say that it doesn't make sense! $E$ is the set of **all** environment states, but $R^E$ may not contain all environment states, if I understood correctly your definitions. I think what confuses you is that you defined a "run" as $\gamma=(e_0, \alpha_0, e_1, \alpha_1, \dots,e_u, \alpha_u)$, which makes you think that it contains all environment states, but intuitively that doesn't seem to be necessarily the case.
Comments.UserDisplayName: nbro
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-02-19T06:04:11.937Z
Comments.Text: I'll correct the definitions. Also, I think you've correctly pointed out the flaw in my assumptions.
Comments.UserDisplayName: aidar_ms
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-02-19T06:35:19.150Z
Comments.Text: But i think with chess example it makes a bit more sense (at least I think it started to :D). $E$ is all legal positions; $Ac$ is all legal moves; $r$ is a game (sequence of positions and moves); $R$ is a set of all such possible games; $R^{Ac}$ is a subset of $R$, set of sequences that end with a move;  $R^E$ is a subset of $R$, set of sequences that end with a position. I think theoretically we can see that $R^E$, being a set of all possible games that with a position, **does encompass** $E$
Comments.UserDisplayName: aidar_ms
Comments.ContentLicense: CC BY-SA 4.0
Comments.CreationDate: 2020-02-19T12:37:05.867Z
Comments.Text: *being a set of all possible games that **end** with a position
Comments.UserDisplayName: aidar_ms
Tags: <math><multi-agent-systems>
Title: Formal proof that every purely reactive agent has behaviorally equivalent standard agent
UserDisplayName: aidar_ms
ThreadText: # Formal proof that every purely reactive agent has behaviorally equivalent standard agent
  
  (Asked by: username_0 on 2020-02-18)
  
  It kind of makes sense intuitively but I'm not sure about a formal proof. I'll start with briefly listing definitions from **Intro to Multiagent systems, Wooldridge, 2002** and then give you my reasoning attempts thus far.
  
  $E$ is a finite set of discrete, instantaneous states, $E=(e, e',...)$. $Ac$ is a repertoire of possible actions (also finite) available to an agent, which transform the environment, $Ac=(\alpha, \alpha', ...)$. A run is a sequence of interleaved environment states and actions, $r=(e\_0, \alpha\_0, e\_1, \alpha\_1,..., \alpha\_{u-1}, e\_u)$, set of all such possible finite sequences (over $E$ and $Ac$) is $R$, $R^E$ is a subset of $R$ containing the runs that end with an env. state.
  
  Purely reactive agent is modeled as: $Ag\_{pure}: E\mapsto Ac$, a standard agent is modeled as $Ag\_{std}: R^E\mapsto Ac$.
  
  So, if $R^E$ is a sequence of agent's actions and environment states, than it just makes sense that $E\subset R^E$. Hence, $Ag\_{std}$ can map to every action to which $Ag\_{pure}$ can. And behavioral equivalence with respect to environment $Env$ is defined as $R(Env, Ag\_{1}) = R(Env, Ag\_{2})$; where $Env=\langle E,e\_{0},t \rangle$, $e\_{0}$ - initial environment state, $t$ - transformation function (definition irrelevant for now).
  
  Finally, if $Ag\_{pure}: E\mapsto Ac$ **and** $Ag\_{std}: R^E\mapsto Ac$, **and** $E\subset R^E$, we can say that $R(Env,Ag\_{pure}) = R(Env, Ag\_{std})$ (might be too bold of an assumption). Hence, every purely reactive agent has behaviorally equivalent standard agent. The opposite might not be true, since $E\subset R^E$ means that all elements of $E$ belong to $R^E$, while not all elements $R^E$ belong to $E$.
  
  It's a textbook problem, but I couldn't find an answer key to check my solution. If anyone has formally (and perhaps mathematically) proven this before, can you post your feedback, thoughts, proofs in the comments? For instance, set of mathematical steps to infer $E\subset R^E$ from their definitions: $E=(e\_{0}, e\_{1},..., e\_{u})$ and $R^E$ is "*all agent runs that end with an environment state*" (no formal equation found) is not clear to me.
  
  **Tags:** math, multi-agent-systems
  > **Comments:**
  > **username_1**: Hi and welcome to AI SE. You say "if $R^E$ is a sequence of agent's actions and environment states, than it just makes sense that $E \subset R^E$", but I would say that it doesn't make sense! $E$ is the set of **all** environment states, but $R^E$ may not contain all environment states, if I understood correctly your definitions. I think what confuses you is that you defined a "run" as $\gamma=(e_0, \alpha_0, e_1, \alpha_1, \dots,e_u, \alpha_u)$, which makes you think that it contains all environment states, but intuitively that doesn't seem to be necessarily the case.  
  > **username_0**: I'll correct the definitions. Also, I think you've correctly pointed out the flaw in my assumptions.  
  > **username_0**: But i think with chess example it makes a bit more sense (at least I think it started to :D). $E$ is all legal positions; $Ac$ is all legal moves; $r$ is a game (sequence of positions and moves); $R$ is a set of all such possible games; $R^{Ac}$ is a subset of $R$, set of sequences that end with a move;  $R^E$ is a subset of $R$, set of sequences that end with a position. I think theoretically we can see that $R^E$, being a set of all possible games that with a position, **does encompass** $E$  
  > **username_0**: *being a set of all possible games that **end** with a position  
  
  ---
  
  ## 2 answers
  
  ### Answer by username_2 on 2021-01-20. Score: 0
  
  **This is how I see it:**
  
  The state that a purely reactive agent is reacting to is, in fact, a subset of the set of all possible runs that end with a state. So in theory, *E* (some state) is a subset of *R* (finite set of all possible runs with a state as the last element). Standard and purely reactive agents are similar in the sense that the agents' purpose is to commit an action given some condition. It is entirely possible that a standard agent might be dealing with a run which encompasses only one element. Therefore, this would imply that for a discrete event in time, the standard agent's behaviour would be equivalent to a purely reactive agent, right? or am I completely off the rails?
  
  Sorry for not using the required symbols, I'm new here and am getting used to the styling :D
  
  > **Comments:**
  > **username_2**: I think there needs to be a better definition for individual states. In your case and my case, we are implying that *E* is a subset of *R*, however, in that case, we are implying a whole set of elements, as opposed to any individual element. A whole run may not have all the states in the set *E*, however it would require at least **one state**.  Therefore any particular element in the set *E* is a subset of *R*, and therefore, for every possible purely reactive agent that is reacting to some state *e* ∈ *E*, there is a behaviourally equivalent standard agent  
  
  ---
  
  ### Answer by username_3 on 2020-02-19. Score: 0
  
  I recommend you to look into the literature about simulation and bisimulation in Automata Theory and its applications to model checking (where you want to make quite regularly proofs of "behavioural equivalence"). One article that discusses this in the context of a technique for model checking known as "Abstraction and Abstraction Refinement" is
  Abstraction and Abstraction Refinement
  Dennis Dams and Orna Grumberg
  In Springer's Handbook of Model Checking, 2018, Chapter 13, pages 385-420
  
  A good (I use it regularly) book that covers behavioural equivalence for a wide variety of automata is 
  Verification and Control of Hybrid Systems: A Symbolic Approach
  Paulo Tabuada
  Springer, 2009
  
  > **Comments:**
  > **username_0**: Thanks for the suggested readings. Will definitely take a look  
  
  ---
  
  