loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06)
CTL Model Checking for Labelled Tree Queries
Budapest, Hungary
June 15-June 17
ISBN: 0-7695-2617-9
Sylvain Halle, Universite du Quebec a Montreal, Canada
Roger Villemaire, Universite du Quebec a Montreal, Canada
Omar Cherkaoui, Universite du Quebec a Montreal, Canada
Querying and efficiently validating properties on labelled tree structures has become an important part of research in numerous domains. In this paper, we show how a fragment of XPath called Configuration Logic (CL) can be embedded into Computation Tree Logic. This framework embeds into CTL a larger subset of XPath than previous work and in particular allows universally and existentially quantified variables in formulas. Finally, we show how the variable binding mechanism of CL can be seen as a branching-time equivalent of the "freeze" quantifier.
Citation:
Sylvain Halle, Roger Villemaire, Omar Cherkaoui, "CTL Model Checking for Labelled Tree Queries," time, pp.27-35, Thirteenth International Symposium on Temporal Representation and Reasoning (TIME'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.