The model is responsible for simulating the physical behavior in different robotics manipulation tasks. For each input signal, i.e., the initial configuration, a trained AI software controller attempts to control the manipulator to accomplish the task. This results in a sequence of observations, i.e., the system trajectory, that will be used in the monitor to verify the completeness of the task. As aforementioned, in our benchmark, each task is wrapped as an Omniverse Isaac Gym environment. To facilitate compatibility with other physical simulators, we further wrap all task environments into standard OpenAI Gym environments by using the wrapper provided in the SKRL library. This enables the developed falsification framework to be used not only with Isaac Sim but also with other physical simulators that utilize OpenAI Gym environments, e.g., Mujoco or PyBullet.

The monitor takes the system trajectory generated from the simulation as input and computes the robustness of the AI controller's behavior against predefined STL specifications. We use RTAMT, a Python library for monitoring STL specifications, to compute the robustness values.

The optimizer searches for worst-case scenarios where the AI controller fails to meet the STL specifications, i.e., the initial configurations resulting in a system trajectory with minimal robustness.  Such a search process is considered an optimization problem where the objective function is the combination of the model and the monitor, which returns the corresponding robustness value for a given input signal. We implement three optimization algorithms, namely random, Nelder-Mead, and dual annealing, in the proposed falsification framework. The latter two algorithms are based on the Scipy library.