Real-time, Online, Low-Impact Temporal Pattern Matching

A temporal pattern matching technique based on formal specifications using Linear-Time Temporal Logic (LTL) is described. The method is based on Remote Execution and Monitoring (REM) of LTL assertions. Unlike verification applications where the formal specification is used to lo-cate errors in a corresponding program, REM is not con-cerned with correctness but rather with temporal pattern detection. Unlike comparable techniques, such as SQL in temporal databases, the method is completely on-line and does not require storage of the input sequence. This makes REM especially suitable for low-impact, real-time, tempo-ral pattern matching of potentially never ending applica-tions such as security monitoring and financial temporal business rule checking.