Search

Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities. After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O(n[[theta].sup.2]) and space O(n[theta]), where n is the size of the recursive machine and [theta] is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node. Categories and Subject Descriptors: D.2.2 [Software Engineering]: Design Tools and Techniques--State diagrams; D.2.4 [Software Engineering]: Software/Program Verification--Formal methods; F.1.1 [Computation by Abstract Devices]: Models of Computation--Automata; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs General Terms: Verification, Algorithms Additional Key Words and Phrases: Software verification, recursive state machines, pushdown automata, context-free languages, model checking, temporal logic, program analysis

Symmetry reduction methods exploit symmetry in a system in order to efficiently verify its temporal properties. Two problems may prevent the use of symmetry reduction in practice: (1) the property to be checked may distinguish symmetric states and hence not be preserved by the symmetry, and (2) the system may exhibit little or no symmetry. In this article, we present a general framework that addresses both of these problems. We introduce "Guarded Annotated Quotient Structures" for compactly representing the state space of systems even when those are asymmetric. We then present algorithms for checking any temporal property on such representations, including non-symmetric properties. Categories and Subject Descriptors: D.1.3 [Programming Techniques]: Concurrent Programming; D.2.4 [Software Engineering]: Software/Program Verification--formal methods; model checking; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--mechanical verification General Terms: Verification, Reliability, Theory Additional Key Words and Phrases: State space explosion, symmetry reductions, model checking algorithms and tools, temporal logics, formula decomposition