We briefly present a rule-based framework, called EAGLE, shown to be capable of defining and implementing finite trace monitoring logics, including future and past time temporal logic, extended regular expressions, real-time and metric temporal logics (MTL), interval logics, forms of quantified temporal logics, and so on. In this paper we focus on a linear temporal logic (LTL) specialisation of EAGLE. For an initial formula of size m, we establish upper bounds of 0(m^2 2^m \log m) and 0(m^4 2^{2m} \log ^2 m) for the space and time complexity, respectively, of single step evaluation over an input trace. This bound is close to the lower bound 0(2^{\sqrt m }) for future-time LTL presented in [18]. EAGLE has been successfully used, in both LTL and metric LTL forms, to test a real-time controller of an experimental NASA planetary rover.
Citation:
Howard Barringer, Allen Goldberg, Klaus Havelund, Koushik Sen, "Program Monitoring with LTL in EAGLE," ipdps, vol. 17, pp.264b, 18th International Parallel and Distributed Processing Symposium (IPDPS'04) - Workshop 16, 2004