# Formal proof that every purely reactive agent has behaviorally equivalent standard agent

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.

• 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.
– nbro
Feb 19 '20 at 1:07
• I'll correct the definitions. Also, I think you've correctly pointed out the flaw in my assumptions. Feb 19 '20 at 6:04
• 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$ Feb 19 '20 at 6:35
• *being a set of all possible games that end with a position Feb 19 '20 at 12:37

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