Project mentor: Kristin Yvonne Rozier

A temporal logic is a formal system of syntax rules and semantics that allows us to represent and reason about propositions qualified in terms of time. One of the most widely used and well-known temporal logics is Linear-time Temporal Logic (LTL), for which time is conceived as a linear, discrete succession of time instances. LTL extends the classical propositional language by adding temporal operators G, X, and U, with intended meaning as follows:

- Gp: "It will always be the case that p;"

- Xp: "Next time will be the case that p;"

- pUq: "p will be the case until a time when q is the case."

This logic expresses properties that describe the specifications of a system, that is, the behaviors the system should exhibit. For example, the specification “Every request is followed by a grant” can be formalized in LTL as G(request→¬G¬grant). LTL formulas are interpreted over the set of natural numbers with its usual order, where each number represents a time instance, with zero representing the current one, plus an interpretation function (aka a trace) V that assigns to each proposition p a set of time instances V(p)⊆AP on which it holds.

On the other hand, Mission-Time Temporal Logic (MLTL) follows the syntax of LTL while adding finite, discrete, closed-interval bounds on the temporal operators. For example, the formula "G[2,5]p" captures that "p must hold between 2 and 5 time steps from now." MLTL has been used as the specification logic for NASA’s Robonaut2 verification project, as well as for both design-time and runtime verification of the NASA Lunar Gateway Vehicle System Manager. MLTL formulas are interpreted over finite traces, that is, over an initial segment of the set of natural numbers (instead of infinite traces), which may or may not be long enough to cover all the intervals in the formula.

A natural question to ask about any logical formula is to determine whether or not it is satisfiable (i.e., that is true in some interpretation), as well as determining if a given formula is a tautology (i.e., is it always true regardless of its interpretation). In the case of LTL, multiple solutions to these questions have been developed using Büchi Automata, which are essentially finite directed graphs with labeled vertices and edges. However, for MLTL, there is no known good solution, other than encoding each formula into another logic, such as LTL, at an exponential cost, then using algorithms developed for that logic. This project will investigate algorithmic methods to produce automata-based encodings for MLTL formulas that avoid encoding them into LTL first and evaluating their complexity and performance against the best algorithms known for LTL.

Prerequisites:  Basic programming skills, some background in discrete mathematics (introductory undergraduate level), and mathematical maturity. Familiarity with concepts from mathematical logic (satisfiability, soundness, completeness, compactness, etc.) is desirable.