Linear Temporal Logic and Timeline Visualization

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.