Hyperdocuments as automata
- 1 January 1998
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Information Systems
- Vol. 16 (1) , 1-30
- https://doi.org/10.1145/267954.267955
Abstract
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.Keywords
This publication has 20 references indexed in Scilit:
- Interpreted collaboration protocols and their use in groupware prototypingPublished by Association for Computing Machinery (ACM) ,1994
- State-based model checking of event-driven system requirementsIEEE Transactions on Software Engineering, 1993
- HAM: a general purpose hypertext abstract machineCommunications of the ACM, 1988
- Reflections on NoteCards: seven issues for the next generation of hypermedia systemsCommunications of the ACM, 1988
- Research on Automatic Verification of Finite-State Concurrent SystemsAnnual Review of Computer Science, 1987
- Temporal Logic of ProgramsPublished by Springer Nature ,1987
- Multimedia document presentation, information extraction, and document formation in MINOS: a model and a systemACM Transactions on Information Systems, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- A logic-based calculus of eventsNew Generation Computing, 1986
- Mechanizing temporal knowledgeArtificial Intelligence, 1977