‹Programming› 2023
Mon 13 - Fri 17 March 2023 Tokyo, Japan
Wed 15 Mar 2023 16:00 - 16:30 at Faculty of Engineering Building 2, Room 212 - Research Papers 3 Chair(s): Ian Sweet

Linear Temporal Logic (LTL) has been used widely in verification. Its importance and popularity have only grown with the revival of temporal logic synthesis, and with new uses of LTL in robotics and planning activities. All these uses demand that the user have a clear understanding of what an LTL specification means.

Despite the growing use of LTL, no studies have investigated the misconceptions users actually have in understanding LTL formulas. This paper addresses the gap with a first study of LTL misconceptions.

We study researchers’ and learners’ understanding of LTL in four rounds (three written surveys, one talk-aloud) spread across a two-year timeframe. Concretely, we decompose “understanding LTL” into three questions. A person reading a spec needs to understand what it is saying, so we study the mapping from LTL to English. A person writing a spec needs to go in the other direction, so we study English to LTL. However, misconceptions could arise from two sources: a misunderstanding of LTL’s syntax or of its underlying semantics. Therefore, we also study the relationship between formulas and specific traces.

We find several misconceptions that have consequences for learners, tool builders, and designers of new property languages. These findings are already resulting in changes to the Alloy modeling language. We also find that the English to LTL direction was the most common source of errors; unfortunately, this is the critical “authoring” direction in which a subtle mistake can lead to a faulty system. We contribute study instruments that are useful for training learners (whether academic or industrial) who are getting acquainted with LTL, and we provide a code book to assist in the analysis of responses to similar-style questions.

Our findings are grounded in the responses to our survey rounds. Round 1 used Quizius to identify misconceptions among learners in a way that reduces the threat of expert blind spots. Rounds 2 and 3 confirm that both additional learners and researchers (who work in formal methods, robotics, and related fields) make similar errors. Round 4 adds deep support for our misconceptions via talk-aloud surveys.

This work provides useful answers to two critical but unexplored questions: in what ways is LTL tricky and what can be done about it? Our survey instruments can serve as a starting point for other studies.

Wed 15 Mar

Displayed time zone: Osaka, Sapporo, Tokyo change

16:00 - 17:30
Research Papers 3Research Papers at Faculty of Engineering Building 2, Room 212
Chair(s): Ian Sweet Galois, Inc.
16:00
30m
Talk
Little Tricky Logic: Misconceptions in the Understanding of LTLVol. 7remote
Research Papers
Ben Greenman Brown University, Sam Saarinen Brown University, Tim Nelson Brown University, Shriram Krishnamurthi Brown University, United States
Link to publication
16:30
30m
Talk
Building a Secure Software Supply Chain with GNU GuixVol. 7remote
Research Papers
Ludovic Courtès Inria, France
Link to publication
17:00
30m
Talk
Technical Dimensions of Programming SystemsVol. 7remote
Research Papers
Joel Jakubovic University of Kent, Jonathan Edwards Independent, Tomas Petricek Charles University
Link to publication