论文标题
逻辑很小的逻辑：理解LTL的误解
Little Tricky Logic: Misconceptions in the Understanding of LTL
论文作者
论文摘要
上下文：线性时间逻辑（LTL）已被广泛用于验证。它的重要性和受欢迎程度只会随着时间逻辑综合的复兴以及LTL在机器人技术和计划活动中的新用途而增长。所有这些都要求用户清楚地了解LTL规范的含义。 询问：尽管LTL的使用越来越多，但没有研究用户在理解LTL公式方面实际上遇到的误解。本文通过首次研究LTL误解来解决差距。 方法：我们研究研究人员和学习者对LTL的理解，分别是四个回合（三个书面调查，一项对话），分布在两年的时间内。具体而言，我们将“理解LTL”分解为三个问题。阅读规格的人需要了解它在说什么，因此我们研究了从LTL到英语的映射。编写规格的人需要朝另一个方向发展，因此我们将英语学习到LTL。但是，误解可能来自两个来源：对LTL语法或其基本语义的误解。因此，我们还研究公式与特定痕迹之间的关系。 知识：我们发现一些误解对学习者，工具建设者和新财产语言的设计师产生了影响。这些发现已经导致了合金建模语言的变化。我们还发现，英语向LTL方向是最常见的错误来源。不幸的是，这是一个关键的“创作”方向，其中一个微妙的错误可能导致系统错误。我们为熟悉LTL的培训学习者（无论是学术还是工业）有用的学习工具，我们提供了一本代码簿，以协助分析对类似问题的回答。 基础：我们的发现基于对我们的调查回应的回应。第一轮使用Quizius以减少专家盲点威胁的方式来识别学习者之间的误解。第2和第3轮证实，其他学习者和研究人员（以正式方法，机器人技术和相关领域的工作）都犯了类似的错误。第4轮通过Tall-Aroud调查为我们的误解提供了深厚的支持。 重要的是，这项工作为两个关键但未开发的问题提供了有用的答案：LTL棘手是什么，可以做什么？我们的调查工具可以作为其他研究的起点。
Context: 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. Inquiry: 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. Approach: 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. Knowledge: 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. Grounding: 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. Importance 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.
