- In the area of Semistructured Databases and Web Databases, I focused on languages and algorithms for querying web-databases.
- In
A. Cortesi, A. Dovier, E. Quintarelli, and L. Tanca.

Operational and abstract semantics of the query language G-log.

Theoretical Computer Science, 275/1-2 pp 521-560, 28 March 2002.we have analyzed the existing graphical query language G-log. Since DB instances (even web sites) are (labeled) graphs and in G-log queries are exactly graphs, it can be shown that retrieving information amounts to finding subgraphs of the instances that "matches" the query graph. In this paper we have shown that the bisimulation test is what really needed for implementing the "matching" test. The results are for the language G-log but are immediately applicable to any language that deals with "graph-based" DBs.

- Bisimulation reflects the intuitive semantics of the
query better than other graph equivalences (e.g.
Isomorphism). Moreover, from the computational point of
view, while no one knows if the isomorphism test admits
an algorithm in P, fast algorithms exist for testing
whether two graphs (with or without labels) are
equivalent.
For instance, in:
A. Dovier, C. Piazza, and A. Policriti.

An Efficient Algorithm for Computing Bisimulation Equivalence.

Theoretical Computer Science 311(1-3):221-256, 2004.we show that the bisimulation test can be computed in O(E log N) or even in O(E + N) if the graphs are acyclic or in some other, well-characterized, cases.

- Unfortunately, in retrieving information we do not
want to see if the complete DB instance is bisimilar to
a query, but finding the subgraphs that are bisimilar to the
query. This problem is shown to be NP-complete in:
A. Dovier and C. Piazza.

The Subgraph Bisimulation Problem.

IEEE Transaction on Knowledge and Data Engineering, vol 15, n. 4, 2003. - Then we observed that finding subgraphs of a graph bisimilar to a given
one is the same kind of activity typically done in model checking:
one need to find the states (nodes) of a transition system (labeled graph)
that satisfy a certain formula. Formulas of CTL are exactly those formulas
that can be represented by a (tree) graph. In:
A. Dovier and E. Quintarelli.

Model Checking Based Data Retrieval.

In Proc. of Database Programming Languages,8th International Workshop on Databases and Programming Languages, DBPL 2001, Revised Papers. LNCS 2397, pages. 62--77. Springer 2002.we have shown how most typical DB queries can be naturally encoded into CTL formulas and therefore that the query retrieval activity is equivalent to solving the model checking problem. For CTL, it can be solved in time LINEAR wrt the product of the size of the graph (DB) and the size of the query (the CTL formula). With these ideas, extracting information from Web-Databases becomes feasible and, moreover, we can also have a purely logical characterization of this activity.

- The extended version of that paper is:

Agostino Dovier and Elisa Quintarelli.

Applying Model-Checking to solve Queries on Semistructured Data

Computer Languages, Systems & Structures.. 25 (2009) pp. 143-172.