One of the goals of this workshop is to identify SAT solving techniques essential to application settings. Aerospace operational concepts are often specified with timelines; we find the Boolean variables and propositional clauses of traditional propositional SAT laid out over time. Therefore, we capture these industrial requirements in Linear Temporal Logic; we must efficiently check LTL satisfiability in order to assure correctness of these requirements before we use them for further analysis, such as model checking or runtime monitoring. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability.

We have established LTL satisfiability checking as a sanity check: each system requirement, its negation, and the set of all requirements should be checked for satisfiability before being utilized for other tasks. We demonstrated that LTL satisfiability checking reduces to model checking, and developed new encodings that performed significantly, sometimes exponentially, better than was previously possible. Others then built on our work to create new stand-alone tools for LTL Satisfiability. However, the state of the art leaves many open questions for future applications of LTL satisfiability.

BIO:

Kristin Yvonne Rozier heads the Laboratory for Temporal Logic in Aerospace Engineering at Iowa State University; previously she spent 14 years as a Research Scientist at NASA. She earned her Ph.D. from Rice University and B.S. and M.S. degrees from The College of William and Mary. Her advances in computation for the aerospace domain earned her many awards including: the NSF CAREER Award; NASA Early Career Faculty Award; American Helicopter Society's Howard Hughes Award; Women in Aerospace Inaugural Initiative-Inspiration-Impact Award; two NASA Group Achievement Awards; two NASA Superior Accomplishment Awards; the Lockheed Martin Space Operations Lightning Award; AIAA's Intelligent Systems Distinguished Service Award. She is an Associate Fellow of AIAA.