Abstract
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 O(m22m log m) and O(m42 2mlog2 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 [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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings - International Parallel and Distributed Processing Symposium, IPDPS 2004 (Abstracts and CD-ROM)|Proc. Int. Parall. Distrib. Process. Symp. IPDPS 2004 |
| Publisher | IEEE Computer Society |
| Pages | 3617-3624 |
| Number of pages | 7 |
| Volume | 18 |
| ISBN (Print) | 0769521320, 9780769521329 |
| Publication status | Published - 2004 |
| Event | Proceedings - 18th International Parallel and Distributed Processing Symposium, IPDPS 2004 (Abstracts and CD-ROM) - Santa Fe, NM Duration: 1 Jul 2004 → … http://dblp.uni-trier.de/db/conf/ipps/ipdps2004-w10.html#CooperDKKMMMMBCCDLOSXJLPRDMSYD04http://dblp.uni-trier.de/rec/bibtex/conf/ipps/CooperDKKMMMMBCCDLOSXJLPRDMSYD04.xmlhttp://dblp.uni-trier.de/rec/bibtex/conf/ipps/CooperDKKMMMMBCCDLOSXJLPRDMSYD04 |
Conference
| Conference | Proceedings - 18th International Parallel and Distributed Processing Symposium, IPDPS 2004 (Abstracts and CD-ROM) |
|---|---|
| City | Santa Fe, NM |
| Period | 1/07/04 → … |
| Internet address |