Hyperdocuments as automata: verification of trace-based browsing properties by model checking Academic Article uri icon


  • 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 thought of as defining an abstract program, termed the links-automaton of the document. A branching temporal logic notation, termed HTL*, is introduced for specifying properties a document should exhibit during browsing. An automated program verification technique called model checking is used to verify that browsing specifications in a subset of HTL* are met by the behavior defined in the links-automation. We illustrate the generality of these techniques by applying them first to several Trellis documents and then to a Hyperties document.

published proceedings

  • ACM Transactions on Information Systems

altmetric score

  • 3

author list (cited authors)

  • Stotts, P. D., Furuta, R., & Cabarrus, C. R.

citation count

  • 53

complete list of authors

  • Stotts, P David||Furuta, Richard||Cabarrus, Cyrano Ruiz

publication date

  • January 1998