A trace semantics for Positive Core XPath

Pieter H. Hartel

    Research output: Book/ReportReportProfessional

    4 Citations (Scopus)
    132 Downloads (Pure)


    We provide a novel trace semantics for positive core XPath that exposes all intermediate nodes visited by the query engine. This enables a detailed analysis of all information relevant to the query. We give two examples of such analyses in the form of access control policies. We translate positive core XPath into Linear Temporal Logic, showing that branching structures can be linearised effectively. The translation is proved correct. We use the SPIN model checker in a proof of concept implementation to resolve the queries, and to perform the access control. The performance of the implementation is shown to be competitive.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages12
    Publication statusPublished - Jan 2005

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    ISSN (Print)1381-3625


    • SCS-Cybersecurity


    Dive into the research topics of 'A trace semantics for Positive Core XPath'. Together they form a unique fingerprint.

    Cite this