Master Thesis Proposal

STL Satisfaction Visualization for Temporal Logic Inference
Co-Supervisors:  Christian Pek (pek2@kth.se), Alexis Linard (linard@kth.se)
Examiner: Jana Tumova
Starting date: ASAP
Project description:

Signal Temporal Logic (STL) [1] is a formalism used in robotics to specify complex tasks and to characterize (desired) behaviours of systems in a machine-interpretable way. However, designing a temporal logic formula is usually a tedious task, often requiring manual tuning. In previous work [2], we developed a learning-based approach that infers an STL specification of a given system by interacting with this system. In the inference process, the learning algorithm generates example signals to ask the system whether the signal satisfies the system’s specification. Based on the result obtained from the system, the learning algorithm iteratively updates its guess of the specification until it converges towards the implemented specification.

Take, for instance, the example of a robot for which we want to infer a specification describing allowed trajectories in a busy environment. To improve the inference approach, we envision incorporating guidance from a human expert. Therefore, the learning algorithm needs to generate positive (i.e. complying with the specification) and negative signals (i.e. violating the specification) and visualize those so that the human expert can judge their membership. Moreover, the human expert may also draw  example signals which can be used by the learning algorithm to improve the inferred specification further. With this new system, we hope to accelerate the learning process, to generate more expressive specifications, and to treat the human expert as another source to retrieve information on the system.

Your task will be two-fold:

1. develop a signal generation approach that is capable of generating a variety of example signals (positive as well as negative) from a given STL specification. This set of signals should be representative of the maximum set of acceptable signals of that specification and be graphically presented to a human expert for labelling.

2. develop a visualization of the satisfaction area of the specification so that the human expert can evaluate the whole specification learnt so far by the algorithm. This may involve the calculation and display of satisfaction boxes of the STL formula [3], or the adaptation of tools initially designed for other formalisms [4].

In this thesis, you will focus on the example of autonomous driving. You will use the CommonRoad framework [5] to visualize the signals. Within this environment, you further develop an approach to integrate a human expert into the existing membership/equivalence query module of the learning algorithm of [2]. Based on examples that you choose (e.g., learning traffic rules) and ground truth data, you demonstrate the effectiveness of your developed system and compute performance metrics (e.g., tightness). In addition, you can benchmark your system against our existing system to investigate whether the human expert supports the inference process.

References

[1] O. Maler and D. Nickovic, “Monitoring temporal properties of continuous signals,” In Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems. Springer, 2004, pp. 152–166.

[2] A. Linard and J. Tumova, “Active Learning of Signal Temporal Logic Specifications,” To appear in Proc. of the IEEE 15th Int. Conf. on Automation Science and Engineering (CASE). 2020.

[3] C. Madsen, P. Vaidyanathan, S. Sadraddini, C.-I. Vasile, N. A. De-Lateur, R. Weiss, D. Densmore, and C. Belta, “Metrics for signal temporal logic formulae,” in Proc. of the IEEE Int. Conf. on Decision and Control (CDC). 2018, pp. 1542–1547.

[4] B. Hohxha, N. Mavridis, G. Fainekos: VISPEC: A graphical tool for elicitation of MTL requirements. In Proc. of the IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS). 2015.

[5] https://commonroad.in.tum.de/scenarios/