An official website of the United States government
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}$$ in threeltl-aware audiences, and misconceptions about standardltlin novices. We find several mistakes, even among experts. In addition, the data supports several categories of errors in both$$\textsc {ltl}_{f}$$ andltlthat have not been identified in prior work. These findings, based on data from actual users, offer insights into whatspecific waystemporal logics are tricky and provide a groundwork for future interventions.
more »
« less
Little Tricky Logic: Misconceptions in the Understanding of 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.
more »
« less
- Award ID(s):
- 2227863
- PAR ID:
- 10472726
- Publisher / Repository:
- Programming Journal
- Date Published:
- Journal Name:
- The Art, Science, and Engineering of Programming
- Volume:
- 7
- Issue:
- 2
- ISSN:
- 2473-7321
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
As part of a larger study focused on supporting high school biology teachers' use of productive science talk, this study compares the use of two different observation protocols, the RTOP and the IQA-SOR. Reviewing a year-long data set of video observations collected from classrooms of teachers participating in the larger professional development study, the two validated instruments produced significantly correlated scores of different scales based on the unique structure of each tool. We posit this demonstrates that both instruments can be useful for analyzing classroom instruction intended to emphasize productive science talk. However, the instruments do possess unique structural and theoretical qualities that warrant this study to understand the insights afforded by each. The similarities and differences emerging from each are explored in the presentation and how they impact the analyses. These considerations can be helpful for scholars who research in-service teacher learning as classroom implementation and impact on student learning activities are general outcomes that most professional development research endeavors to explore. Further, considerations of what a particular observation protocols’ foci include will be necessary so that continued research on teacher learning works to make science learning through discourse accessible to all learners.more » « less
-
A powerful operational paradigm for distributed quantum information processing involves manipulating pre-shared entanglement by local operations and classical communication (LOCC). The LOCC round complexity of a given task describes how many rounds of classical communication are needed to complete the task. Despite some results separating one-round versus two-round protocols, very little is known about higher round complexities. In this paper, we revisit the task of one-shot random-party entanglement distillation as a way to highlight some interesting features of LOCC round complexity. We first show that for random-party distillation in three qubits, the number of communication rounds needed in an optimal protocol depends on the entanglement measure used; for the same fixed state some entanglement measures need only two rounds to maximize whereas others need an unbounded number of rounds. In doing so, we construct a family of LOCC instruments that require an unbounded number of rounds to implement. We then prove explicit tight lower bounds on the LOCC round number as a function of distillation success probability. Our calculations show that the original W-state random distillation protocol by Fortescue and Lo is essentially optimal in terms of round complexity.more » « less
-
Abstract Issues of intelligibility may arise amongst English learners when acquiring new words and phrases in North American academic settings, perhaps in part due to limited linguistic data available to the learner for understanding language use patterns. To this end, this paper examines the effects of Data‐Driven Learning for Pronunciation (DDLfP) on lexical stress and prominence in the US academic context. 65 L2 English learners in North American universities completed a diagnostic and pretest with listening and speaking items before completing four online lessons and a posttest on academic words and formulas (i.e., multi‐word sequences). Experimental group participants (n = 40) practiced using an audio corpus of highly proficient L2 speakers while comparison group participants (n = 25) were given teacher‐created pronunciation materials. Logistic regression results indicated that the group who used the corpus significantly increased their recognition of prominence in academic formulas. In the spoken tasks, both groups improved in their lexical stress pronunciation, but only the DDLfP learners improved their production of prominence in academic formulas. Learners reported that they valued DDLfP efforts for pronunciation learning across contexts and speakers. Findings have implications for teachers of L2 pronunciation and support the use of corpora for language teaching and learning.more » « less
-
Lal, A; Tonetta, S. (Ed.)Reactive synthesis holds the promise of generating automatically a verifiably correct program from a high-level specification. A popular such specification language is Linear Temporal Logic (LTL). Unfortunately, synthesizing programs from general LTL formulas, which relies on first constructing a game arena and then solving the game, does not scale to large instances. The specifications from practical applications are usually large conjunctions of smaller LTL formulas, which inspires existing compositional synthesis approaches to take advantage of this structural information. The main challenge here is that they solve the game only after obtaining the game arena, the most computationally expensive part in the procedure. In this work, we propose a compositional synthesis technique to tackle this difficulty by synthesizing a program for each small conjunct separately and composing them one by one. While this approach does not work for general LTL formulas, we show here that it does work for Safety LTL formulas, a popular and important fragment of LTL. While we have to compose all the programs of small conjuncts in the worst case, we can prune the intermediate programs to make later compositions easier and immediately conclude unrealizable as soon as some part of the specification is found unrealizable. By comparing our compositional approach with a portfolio of all other approaches, we observed that our approach was able to solve a notable number of instances not solved by others. In particular, experiments on scalable conjunctive benchmarks showed that our approach scale well and significantly outperform current Safety LTL synthesis techniques. We conclude that our compositional approach is an important contribution to the algorithmic portfolio of Safety LTL synthesis.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.22152/programming-journal.org/2023/7/7
