I. Introduction
Social navigation of robots among humans is a research topic concentrating much interest due to diverse challenges, such as the prediction of human behavior in crowded social environments to enable efficient robot navigation, or the identification of “navigation styles” for a mobile robot in its surrounding environment [1]. In robot motion planning and control, desired behavior specifications and preferences can be expressed in Signal Temporal Logic (STL) [2], a formalism that can express system properties that include bounds on time and values of system parameters. STL defines specifications over multi -dimensional continuous signals and can, e.g., be used to depict properties of trajectories. Since STL allows rich expressiveness and resemblance to natural language [3], it has recently been used in human-robot interaction applications [4], [5], and human-robot encounters. Indeed, there is a growing need to depict human-robot in-teractions through formal and rigorous techniques to provide guarantees on the functioning of robotic systems, as well as their interactions with humans and perceived safety [6].