Misconceptions in Finite-Trace and Infinite-Trace Linear Temporal Logic

摘要

Abstract With the growing use of temporal logics in areas ranging from robot planning to runtime verification, it is critical that users have a clear understanding of what a specification means. Toward this end, we have been developing a catalog of semantic errors and a suite of test instruments targeting various user-groups. The catalog is of interest to educators, to logic designers, to formula authors, and to tool builders, e.g., to identify mistakes. The test instruments are suitable for classroom teaching or self-study. This paper reports on five sets of survey data collected over a three-year span. We study misconceptions about finite-trace $$\textsc {ltl}_{f}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mstyle> <mml:mi>L</mml:mi> <mml:mi>T</mml:mi> <mml:mi>L</mml:mi> </mml:mstyle> <mml:mi>f</mml:mi> </mml:msub> </mml:math> in three ltl -aware audiences, and misconceptions about standard ltl in novices. We find several mistakes, even among experts. In addition, the data supports several categories of errors in both $$\textsc {ltl}_{f}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msub> <mml:mstyle> <mml:mi>L</mml:mi> <mml:mi>T</mml:mi> <mml:mi>L</mml:mi> </mml:mstyle> <mml:mi>f</mml:mi> </mml:msub> </mml:math> and ltl that have not been identified in prior work. These findings, based on data from actual users, offer insights into what specific ways temporal logics are tricky and provide a groundwork for future interventions.