Rajeev Alur - Ardmore PA
Mihalis Yannakakis - Summit NJ
Lucent Technologies Inc. - Murray Hill NJ
Model checking is applied to a hierarchical state machine (i. e. , a state machine having at least one state (i. e. , a superstate) that is itself a state machine) without first flattening the hierarchical state machine. In one embodiment, the model checking involves one or more or reachability, cycle-detection, linear-time requirements, and branching-time requirements analyses. For reachability analysis, in addition to keeping track of whether states have been visited, the algorithm also keeps track of the exit nodes for each superstate. Cycle-detection analysis has two phases: a primary phase in which target states are identified and a secondary phase in which it is determined whether identified target states are part of closed processing paths or loops. For cycle-detection analysis, the algorithm keeps track of (1) whether states have been visited during the primary phase, (2) the exit nodes for each superstate, and (3) whether states have been visited during the secondary phase. For linear-time requirements analysis, a formula is translated into an automaton, and a product construction is defined between the automaton and a hierarchical machine that yields a new hierarchical machine that is then analyzed using the cycle-detection algorithm.