VISUAL FORMALISM, STATECHARTS, AND STATEMATE Finite-state machines (FSMs) have been used extensively in the specification and analysis of many computer-based as well as non-computer-based systems, ranging from electronic circuits to econometric models. They can model in detail the behavior of a system, and several algorithms exist to perform the analysis. Unfortunately, classical state machines such as those employed in the standard, explicit-state CTL model-checking approach [Clarke, Emerson, an