Navigation in hypertext is easy only sometimes

One of the main unsolved problems confronting Hypertext is the navigation p roblem, namely, the problem of having to know where you are in the database graph representing the structure of a Hypertext database, and knowing how to get to some other place you are searching for in the database graph. In order to tackle this problem we introduce a formal model for Hypertext. In this model a Hypertext database consists of an information repository, whic h stores the contents of the database in the form of pages, and a reachabil ity relation, which is a directed graph describing the structure of the dat abase. The notion of a trail, which is a path in the database graph describ ing some logical association amongst the pages in the trail, is central to our model. We define a Hypertext query language for our model based on a subset of pro positional linear temporal logic, which we claim to be a natural formalism as a basis for establishing navigation semantics for Hypertext. The output of a trail query in this language is the set (which may be infinite) of all trails that satisfy the query. We show that there is a strong connection b etween the output of a trail query and finite automata in the sense that, g iven a Hypertext database and a trail query, we can construct a finite auto maton representing the output of the query, which accepts a star-free regul ar language. We show that the construction of the finite automaton can be d one in time exponential in the number of conjunctions, between the subformu las of the trail query, plus one. Given a Hypertext database and a trail query, the problem of deciding wheth er there exists a trail in the database that satisfies the trail query is r eferred to as the model checking problem. We show that, although this probl em is NP-complete for different subsets of our query language, it can be so lved in polynomial time for some significant special cases. Thus the naviga tion problem can only be efficiently solved in some special cases, and ther efore in practice Hypertext systems could include algorithms which return r andomized and/or fuzzy solutions.