Model-checking based data retrieval. An application to semistructured and temporal data.
type: Item
instance of: scholarly article
title: Model-checking based data retrieval. An application to semistructured and temporal data.
zbMATH Open document ID: 1069.68044
author: Elisa Quintarelli
published in: Lecture Notes in Computer Science
publication date: 2004-09-30T00:00:00Z
review text: The volume contains the results of the research covered by the Ph.D. dissertation of Elisa Quintarelli at the Politecnico di Milano. Two specific problems in the area of representation of semistructured data and queries are addressed -- the study and definition of a semantics for a graph-based query language, and the usage of model-checking based techniques to efficiently solve graphical queries on static and dynamic semistructured documents. In particular, methods for searching on the Web are considered. An effective graph-based approach to the formalization of query languages for semistructured and temporal information is introduced supporting both data structure variability and different topological similarities between queries and document structures. This offers a powerful and flexible paradigm for query execution based on matching the query graph with the database instance graph. Static and temporal queries are naturally expressed by labeled graphs. One of the main contributions is the design of a semantics for the \(G\)-log language based on the notion of bisimulation. It allows different similarity levels to be supported, but in general it is computationally so complex that it is not applicable to real-life-size problems. In order to overcome this limiting but crucial issue, the author observes that the graphical queries can be easily translated into logic formulae. It is possible to associate a modal logic formula \(F\) to a query and to interpret database instance graphs as Kripke Transition Systems (KTS). In this way the problem of solving a graphical query with respect to a semistructured database is reduced to an instance of the model-checking problem. A modal logic with the same syntax as the temporal logic CTL is used; finding subgraphs of the database instance graph that match the query can be performed by finding nodes of the KTS derived from the database instance graph that satisfy the formula \(F\). Then the problem is decidable and algorithms run…
Mathematics Subject Classification ID: 68P20
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 68P15
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68T05
Mathematics Subject Classification ID: 03B70
zbMATH DE Number: 2104434
zbMATH Keywords: semistructured data
zbMATH Keywords: temporal data
zbMATH Keywords: model-checking based data retrieval
describes a project that uses: ELISA
MaRDI profile type: Publication
full work available at URL: b94902
OpenAlex ID: W2611503582
DOI: 10.1007/B94902
Recommended article: Q5714250
Recommended article: Applying model-checking to solve queries on semistructured data
Recommended article: Model checking hybrid logics (with an application to semistructured data)
Recommended article: Q3046899
Recommended article: Database Theory - ICDT 2005
Recommended article: Evaluation of temporal datasets via interval temporal logic model checking
description: scientific article; zbMATH DE number 2104434