HYPERDOCUMENTS AS AUTOMATA - VERIFICATION OF TRACE-BASED BROWSING PROPERTIES BY MODEL CHECKING

We present a view of hyperdocuments in which each document encodes its own browsing semantics in its links. This requires a mental shift in how a hyperdocument is thought of abstractly. Instead of treating the links of a document as defining a static directed graph, they are thou ght of as defining an abstract program, termed the links-automaton of the document. A branching temporal logic notation, termed HTL, is int roduced for specifying properties a document should exhibit during bro wsing. An automated program verification technique called model checki ng is used to verify that browsing specifications in a subset of HTL are met by the behavior defined in the links-automaton. We illustrate the generality of these techniques by applying them first to several T rellis documents and then to a Hyperties document.