What's in a Name? Linear Temporal Logic Literally Represents Time Lines

Linear Temporal Logic (LTL) is arguably the most popular specification language for formal verification of safety-critical systems. However, LTL formulas can be unintuitive and error- prone for human practitioners to specify and validate. Meanwhile, drawing timelines remains one of the most popular methods for specifying and validating requirements for indus-trial system designs, such as in aerospace operational concepts. Therefore, we provide a new timeline tool for visualizing LTL specifications as timelines, providing provably-correct, intuitive equivalents between these two specification formats. Our tool generates timeline visualizations by translating LTL formulas to intermediate representations as Buchi automata and then regular expressions, and finally simplifying and visualizing the expressions. We provide an algorithm for this visualization, a theoretical soundness analysis” and an implementation.