An Empirical Study on the Impact of Example Traces on Linear Temporal Logic Comprehension

Formal specifications support the verification of complex systems and reduce the likelihood of safety-critical errors. However, writing correct specifications is notoriously difficult, posing a significant barrier to their adoption in the industry. In particular, Linear Temporal Logic (LTL), a longstanding standard in computer-aided verification, has been shown to be error-prone and difficult for engineers to read and write correctly. This highlights the need for empirical research to identify supportive techniques that can help address these challenges. In this work, we propose an experiment to measure the impact of providing example traces on LTL formula comprehension of participants with different expertise levels. We consider positive and negative examples in the form of traces that satisfy or violate a given formula. Intuitively, examining examples could help engineers challenge incorrect assumptions or reinforce correct ones. To this end, we collected 46 LTL formulas from several datasets, and defined an example-generation algorithm. Our study consists of two empirical methods: (1) a quantitative randomized test to asses participants’ response times and correctness on a series of comprehension tasks, with and without the aid of example traces, and (2) a qualitative semi-structured interview to explore where and how example traces support LTL comprehension. We recruited 146 respondents for the randomized test and conducted 22 follow-up interviews. Our statistical analysis shows that providing example traces alongside LTL formulas generally increases the time required to answer correctly, while substantially improving novices’ performance to a level comparable to that of experts. Our thematic analysis on the interviews further revealed specific benefits and limitations of example traces. In particular, traces reinforce one’s assumptions, but sometimes have limited coverage.