Formalizing Time: Temporal Logics and the Challenge of Visualizing MLTL

Abstract: Temporal logics are a family of modal logics that reason about timelines. They are usually obtained by expanding classical propositional logic with modal operators that can qualify the value of a proposition over time, such as “p will always be true” or “q is true until p becomes true.” However, different concepts of time are often captured by significant logical systems, as these tend to encode the various characteristics that define them, such as continuous vs. discrete time and linear vs. branching time. The use and development of these logics have been increasing significantly over the last 50 years, as researchers and engineers in fields related to computer science have been using them to verify safety-critical systems in a formal and precise manner.

In this talk, I will introduce some of the better-known temporal logics that aim to formalize different concepts of time and briefly explain the different properties that make them good candidates for use in different computer-based environments. After that, I will focus on a logic I have been working on during my PhD known as Mission-time (Linear) Temporal Logic (MLTL), which is a logic that reasons about finite and discrete timelines (called traces) where finite intervals bound the temporal operators. Although MLTL is only as expressive as classical propositional logic, it has been capturing the attention of multiple research groups in recent years, and its succinctness has shown to become a challenge for engineers easily when trying to validate the formulas they believe are capturing the desired behaviors. For that, at the Laboratory for Temporal Logic at ISU, we have been developing algorithms that allow us to take an MLTL formula and produce a visual representation for the traces that satisfy the formula.

logic in computer sciencesoftware engineeringlogic

Audience: researchers in the topic

Online logic seminar

Series comments: Description: Seminar on all areas of logic