Linear Temporal Logic and Timeline Visualization
Date
2021-12
Authors
Pohlen, Christopher
Major Professor
Rozier, Kristin-Yvonne
Advisor
Committee Member
NA, NA
Journal Title
Journal ISSN
Volume Title
Publisher
Authors
Research Projects
Organizational Units
Journal Issue
Is Version Of
Versions
Series
Department
Abstract
The field of formal methods and requirements specification are difficult topics to learn and can be error prone to utilize. This exploratory work endeavors to lay the groundwork for the eventual creation of a computer-based tool for visualizing Linear Temporal Logic (LTL) as interactive timelines. The proposed tool would be able to take an LTL formula, parse it into a binary tree, and create a timeline by recursively traversing the tree. Any change to the timeline would then have a corresponding change to LTL formula with a one-to-one relationship. Before such a tool can be created, this work looks at producing a survey for finding a Human Factors solution to visualizing the LTL formulas as timelines. The survey produced asks questions about subjective preferences for LTL visualizations and uses the participants’ preferences to ask questions using some basic and a couple complex LTL formulas. Questions are also asked to determine whether participants prefer certain types of formal methods tools over others. The survey will be utilized as a template for continued research into visualizing LTL and eventual creation of the tool.
Comments
Description
Keywords
Citation
DOI
Source
Copyright
2021