The specification of a graphical user interface (GUI), like any other part of a computer system, is an incremental process whereby an outline of the system is systematically developed, evaluated, and revised until it is reasonably complete. This article describes some algorithms and procedures that can be used to automate the analysis of a specification to facilitate this iterative process. A propositional production system (PPS) is a notation that can be used by designers to describe the high-level behavior of a GUI. Such a description is executable and relatively easy to learn and use. PPSs are a form of state machine; therefore, much of the theory of state machines can be applied to their analysis. PPSs, however, provide the advantage of semiparallel definitions of state transitions. This is important, as dialogue models of modem GUIs allow a large number of simultaneously available inputs leading to very large state spaces. By dealing in sets of states, a PPS makes the problem of describing the potentially exponential number of state transitions tractable. This article discusses how this innovation can lead to efficient algorithms for analyzing a dialogue model for properties such as task completeness, reversibility of effect, accessibility, connectedness, and avoidance of deadlock.