Weintroduce anovel encoding forMission-time Linear Temporal Logic (MLTL), inspired by the recently-proposed Temporal Exponential Propagation method forl earning finitetrace Linear Temporal Logic (LTLf) formulas.Our encoding translates MLTL formulas into bit-vector expressions whose size is O(nlog 2 (K)) with n and K being proportional to the formula size and largest temporal intervalpresent in the formula respectively.W edemonstrate howthis encoding can be leveraged fort wo corea pplications: satisfiability checking and runtime monitoring.F or satisfiability,our approach complements existing techniques by efficiently solving instances that arechallenging for traditional encodings.F or runtime monitoring, we showt hato ur method achievess ignificantly higher throughput thanc urrent state-of-the-artt ools, enabling faster and mores calable runtime verification in time-sensitive systems.Experimental results confirm that the proposed encoding and monitoring algorithm provide ap ractical and effective foundation forr easoning about MLTL properties, achieving 10.52 times higher throughput compared to state-of-the-art online techniques over as ample of pattern-instantiated formulas.
Johannsen et al. (Wed,) studied this question.