loading...
Program Monitoring with LTL in EAGLE
Santa Fe, New Mexico April 26-April 30
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/IPDPS.2004.130333618th International Parallel and Distr ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Howard Barringer, University of Manchester
Allen Goldberg, NASA Ames Research Center
Klaus Havelund, NASA Ames Research Center
Koushik Sen, University of Illinois at Urbana Champaign
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
Usage of this product signifies your acceptance of the Terms of Use.


Suggestions