Rozier Gives Invited Talk at AAAI 2023 Spring Symposium Series

On the Effectiveness of Mission-time Linear Temporal Logic (MLTL) in AI Applications

Mission-time Linear Temporal Logic (MLTL) adds closed-interval integer bounds on the temporal operators of LTL, enabling unit-agnostic specification over finite traces. It is arguably the most-used variation of MTL, and the most-used subset of STL in industrial and AI applications. MLTL optimizes the trade-off between expressibility of a wide range of realistic requirements and the ability to author generic, easy-to-validate formulas. We highlight successful AI applications centered around MLTL requirements, including Robonaut2 and the NASA Lunar Gateway Vehicle System Manager. We overview advances in analyzing MLTL, explain the motivation driving these developments, and point out the gaps in the state of the art where there are needs for future work.

Leave a Comment

Filed under Research Talks

Leave a Reply

Your email address will not be published. Required fields are marked *