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

Question

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.

Answer 1

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

Answer 2

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