Linear Temporal Logic and Timeline Visualization

dc.contributor.author Pohlen, Christopher
dc.contributor.committeeMember NA, NA
dc.contributor.majorProfessor Rozier, Kristin-Yvonne
dc.date.accessioned 2022-06-06T17:04:15Z
dc.date.available 2022-06-06T17:04:15Z
dc.date.copyright 2021
dc.date.issued 2021-12
dc.description.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.
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/105206
dc.language.iso en_US
dc.rights.holder Christopher Pohlen
dc.subject.disciplines DegreeDisciplines::Social and Behavioral Sciences::Psychology::Human Factors Psychology
dc.subject.keywords Timelines
dc.subject.keywords Visualization
dc.subject.keywords Human Factors
dc.subject.keywords Formal Methods
dc.subject.keywords Temporal Information
dc.subject.keywords Propositional Logic
dc.title Linear Temporal Logic and Timeline Visualization
dc.type Text
dc.type.genre creativecomponent
dspace.entity.type Publication
thesis.degree.department Aerospace Engineering
thesis.degree.discipline Human Computer Interaction
thesis.degree.level Masters
thesis.degree.name Master of Science
File
Original bundle
Now showing 1 - 1 of 1
Name:
F21-Pohlen-LinearTemporal-CC.pdf
Size:
866.61 KB
Format:
Adobe Portable Document Format
Description: