|
Abstract : |
Abstract. We briefly present a rule-based framework, called EAGLE, that has been 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 show how EAGLE can perform linear temporal logic (LTL) monitoring in an efficient way. For an initial formula of size m, we establish upper bounds of O(m 2 2 m logm) and O(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 O(2 ? m) for future-time LTL presented in [17]. EAGLE has been successfully used, in both LTL and metric LTL forms, to test a real-time controller of an experimental NASA planetary rover. 1, |
