Speaker:Gokul Hariharan

Maximum Satisfiability in Mission-time Linear Temporal Logic

Mission-time Linear Temporal Logic (MLTL) is a popular language for specifications in cyber-physical safety-critical systems. MLTL is a variant of Linear Temporal Logic (LTL) with finite interval bounds on temporal operators. It is often hard to satisfy all requirements; prioritization and trade-offs are always used in designing complex systems. Given a set of specifications, the maximum satisfiability problem (MaxSAT) asks to find the maximum number of specifications that can be simultaneously satisfied. Considering the significant advances in MaxSAT for boolean logic, we develop translations of MLTL to boolean logic. Given an MLTL formula $\phi$ of length $|\phi|$ with maximum interval length $m$, our first translator runs in $\mathcal O(m^{|\phi|})$ time. Performance tests of satisfiability checks on MaxSAT instances show that this exponential translation performs significantly better than the best satisfiability checking approaches reported recently in the literature. Furthermore, we report an improved translation algorithm that runs in $\mathcal O(|\phi|^2m^2)$ time that outperforms the best approaches reported thus far. The new approach is embarrassingly parallelizable to a factor of $|\phi|m$. We contribute to (1) an easy-to-implement translation from MLTL to boolean logic that runs in $\mathcal O(m^{|\phi|})$ time, and (2) an efficient translation that runs in $\mathcal O(|\phi|^2m^2)$ time, and we prove their correctness and runtime. Lastly, (3) we consider example cases of using existing boolean MaxSAT solvers to solve the MLTL MaxSAT problem.

Committee: Tichakorn Wongpiromsarn (major professor), Samik Basu, Gianfranco Ciardo, Kristin-Yvonne Rozier, and Phillip Harrison Jones

Join on Zoom: Please click this URL to start or join. https://iastate.zoom.us/j/96095315410 Or, go to https://iastate.zoom.us/join and enter meeting ID: 960 9531 5410