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
Detecting Preposition Errors to Target Interlingual Errors in Second Language Writing
Second language learners studying languages with a diverse
set of prepositions often find preposition usage difficult to
master, which can manifest in second language writing as
preposition errors that appear to result from transfer from a
native language, or interlingual errors. We envision a digital
writing assistant for language learners and teachers that can
provide targeted feedback on these errors. To address these errors,
we turn to the task of preposition error detection, which
remains an open problem despite the many methods that have
been proposed. In this paper, we explore various classifiers,
with and without neural network-based features, and finetuned
BERT models for detecting preposition errors between
verbs and their noun arguments.
more »
« less
- Award ID(s):
- 1705058
- NSF-PAR ID:
- 10191933
- Date Published:
- Journal Name:
- Proceedings of the 33rd International FLAIRS Conference
- Page Range / eLocation ID:
- 290-293
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
The use of writing-based exercises in a circuit analysis course has shown promise in aiding students likely to struggle in the course by enhancing their conceptual understanding of topics related to DC circuit analysis [1]. As grading of writing samples and providing personalized feedback can be time-intensive, automating the evaluation and feedback processes through use of emerging techniques in natural language processing (NLP) could open the door for more widespread use of such writing exercises across STEM courses, thus benefiting students in most need of assistance. In this paper, the development and initial testing of two web-based writing activities that leverage a basic NLP technique to probe student writing related to DC circuits are described. The first writing exercise has students describe what happens to the power of various elements in a resistive circuit as the value of one of the resistors decreases. The second exercise has students consider situations in which the ideal independent voltage and current source models might fail. Both writing exercises are built from a template that includes several metacognitive prompts to spur self-reflection on the part of the user. A rule-based approach was taken to detect evidence of common misconceptions [2] and errors in student responses, as well as to identify sentences that revealed the student was correctly addressing the problems. Based on identified misconceptions or correct concepts in a student’s writing, the web-based application selects appropriate directed line of reasoning (DLR) feedback paths to attempt to lead the writer to an accurate understanding of the behavior of the circuits in question. Key features of the web-based application template as well as details regarding misconception detection and personalized feedback are described. Student impressions of the value of the DLR feedback is assessed using comments provided by the student within the applications. Planned modifications of the web-based writing exercise template based on this formative assessment will be given and address a broader goal of this work – to develop a web-based template that instructors across STEM disciplines, even those without a background in coding, could use to implement their own conceptual writing exercises.more » « less
-
more » « less
Abstract Feedback is important to improve writing quality; however, to provide timely and personalized feedback is a time-intensive task. Currently, most literature focuses on providing (human or machine) support on product characteristics, especially after a draft is submitted. However, this does not assist students who struggle
during the writing process. Therefore, in this study, we investigate the use of keystroke analysis to predict writing quality throughout the writing process. Keystroke data were analyzed from 126 English as a second language learners performing a timed academic summarization task. Writing quality was measured using participants’ final grade. Based on previous literature, 54 keystroke features were extracted. Correlational analyses were conducted to identify the relationship between keystroke features and writing quality. Next, machine learning models (regression and classification) were used to predict final grade and classify students who might need support at several points during the writing process. The results show that, in contrast to previous work, the relationship between writing quality and keystroke data was rather limited. None of the regression models outperformed the baseline, and the classification models were only slightly better than the majority class baseline (highest AUC = 0.57). In addition, the relationship between keystroke features and writing quality changed throughout the course of the writing process. To conclude, the relationship between keystroke data and writing quality might be less clear than previously posited. -
null (Ed.)People who grow up speaking a language without lexical tones typically find it difficult to master tonal languages after childhood. Accumulating research suggests that much of the challenge for these second language (L2) speakers has to do not with identification of the tones themselves, but with the bindings between tones and lexical units. The question that remains open is how much of these lexical binding problems are problems of encoding (incomplete knowledge of the tone-to-word relations) vs. retrieval (failure to access those relations in online processing). While recent work using lexical decision tasks suggests that both may play a role, one issue is that failure on a lexical decision task may reflect a lack of learner confidence about what is not a word, rather than non-native representation or processing of known words. Here we provide complementary evidence using a picture- phonology matching paradigm in Mandarin in which participants decide whether or not a spoken target matches a specific image, with concurrent event-related potential (ERP) recording to provide potential insight into differences in L1 and L2 tone processing strategies. As in the lexical decision case, we find that advanced L2 learners show a clear disadvantage in accurately identifying tone mismatched targets relative to vowel mismatched targets. We explore the contribution of incomplete/uncertain lexical knowledge to this performance disadvantage by examining individual data from an explicit tone knowledge post-test. Results suggest that explicit tone word knowledge and confidence explains some but not all of the errors in picture-phonology matching. Analysis of ERPs from correct trials shows some differences in the strength of L1 and L2 responses, but does not provide clear evidence toward differences in processing that could explain the L2 disadvantage for tones. In sum, these results converge with previous evidence from lexical decision tasks in showing that advanced L2 listeners continue to have difficulties with lexical tone recognition, and in suggesting that these difficulties reflect problems both in encoding lexical tone knowledge and in retrieving that knowledge in real time.more » « less
-
more » « less
Bilinguals occasionally produce language intrusion errors (inadvertent translations of the intended word), especially when attempting to produce function word targets, and often when reading aloud mixed-language paragraphs. We investigate whether these errors are due to a failure of attention during speech planning, or failure of monitoring speech output by classifying errors based on whether and when they were corrected, and investigating eye movement behaviour surrounding them. Prior research on this topic has primarily tested alphabetic languages (e.g., Spanish–English bilinguals) in which part of speech is confounded with word length, which is related to word skipping (i.e., decreased attention). Therefore, we tested 29 Chinese–English bilinguals whose languages differ in orthography, visually cueing language membership, and for whom part of speech (in Chinese) is less confounded with word length. Despite the strong orthographic cue, Chinese–English bilinguals produced intrusion errors with similar effects as previously reported (e.g., especially with function word targets written in the dominant language). Gaze durations did differ by whether errors were made and corrected or not, but these patterns were similar for function and content words and therefore cannot explain part of speech effects. However, bilinguals regressed to words produced as errors more often than to correctly produced words, but regressions facilitated correction of errors only for content, not for function words. These data suggest that the vulnerability of function words to language intrusion errors primarily reflects automatic retrieval and failures of speech monitoring mechanisms from stopping function versus content word errors after they are planned for production.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
