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
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TIME.2006.11
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. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||