Loading...
Please wait, while we are loading the content...
Similar Documents
Program monitoring with ltl in eagle
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Goldberg, Allen Havelund Sr., Klaus Sen, Koushik Barringer, Howard |
| Copyright Year | 2004 |
| Description | 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) specialization of EAGLE. For an initial formula of size m, we establish upper bounds of O(m(sup 2)2(sup m)log m) and O(m(sup 4)2(sup 2m)log(sup 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(sup square root m) for future-time LTL presented. EAGLE has been successfully used, in both LTL and metric LTL forms, to test a real-time controller of an experimental NASA planetary rover. |
| File Size | 893310 |
| Page Count | 8 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20050010167 |
| Archival Resource Key | ark:/13960/t2z36s560 |
| Language | English |
| Publisher Date | 2004-01-01 |
| Access Restriction | Open |
| Subject Keyword | Computer Programming And Software Controllers Logic Programming Planetary Surfaces Temporal Logic Real Time Operation Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
