Generating Explainable Counterfactual Policies through Temporal Logic Queries

As reinforcement learning (RL) agents are deployed in increasingly complex environments, ensuring that their behavior complies with the user's needs has become a central challenge in eXplainable RL (XRL). An agent's policy may solve a given problem, but some of its choices can seem counter-intuitive or surprising to the user, who may have wished to see the agent accomplish its goal in a different way, and may wonder: what if the agent acted with a different intent in mind? Scenarios that answer this question are called counterfactual policies. In this work, we propose a framework that allows the user to request these alternative policies by formulating preferences about the behavior of the agent. These preferences are expressed in Linear Temporal Logic on finite traces (LTLf), a formal yet intuitive language that allows reasoning about deterministic sequences of actions. We synthesize the corresponding counterfactual policies using a multi-objective reinforcement learning algorithm, which produces a diverse set of alternative strategies balancing the agent's original policy with the one envisioned by the user. By comparing these strategies, our framework sheds light on the rationale behind the agent's decisions. Experimental trials show that such a set of policies can be synthesized in reasonable time.