Hfsm

Formal Analysis of Hierarchical State Machines Rajeev Alur
University of Pennsylvania

In honor of Zohar Manna Taormina, June 2003

State-Machine Based Modeling
x x++ x==5 ->x=0

Finite State Machines

Extended FSMs

a

a

Concurrent FSMs Hierarchical FSMs

Hierarchy -> Succinctness
q Concurrent FSMs are exponentially more succinct than FSMs q Extended FSMs (booleanvariables) are also exponentially more succinct q Hierarchical FSMs are also exponentially more succinct than FSMs due to sharing q Intuition: can count succinctly: e.g. can express an with log n levels of nesting

Motivation
q Concurrent FSMs and Extended FSMs well understood and supported by model checkers q Hierarchy common in modern software design languages (e.g. Statecharts, UML) q Goal 1:Theoretical foundations for hierarchical state machines (succinctness, complexity, formal semantics, ….) q Goal 2: What’s the best way to analyze Hierarchical FSMs ? (avoid flattening, exploit hierarchy/sharing)

Hierarchical State Machine
A1 A2 A3 Node Entry node A2 A3 A3 Box (superstate)

A3

Exit node

Reachability
q Underlying transition system (expansion)
§ State records context (seqof boxes) and node § Transitions: internal, calls, returns § Size: exponential in nesting depth (bound is tight)

qConcurrent FSMs are exponentially more expensive than FSMs (PSPACE complete) q Extended FSMs (boolean variables) are also exponentially more expensive (PSPACE complete) q Reachability for Hierarchical FSMs is in P q Intuition: Every nested FSM needs to be searched just once for eachentry point

Reachability
qOn-the-fly enumerative search algorithm tabulates the results of searching a component

qComplexity bound: PTIME complete q O(n k2) algorithm where n is total size, and k = maxi min (entry, exit nodes of component Ai)

Talk Outline
ü Motivation Ü Automata and Succinctness q Temporal Logic Model Checking q Modeling Language and Tool

Hierarchical Automata
qHierarchical state machines with edges labeled by alphabet symbols, and initial/final nodes can be viewed as language generators q {w # wR | |w| = n} has O(n) generator q Language emptiness: easy (same as reachability) q Emptiness of intersection of 2 automata is Pspacecomplete q Universality and language equivalence are Expspacecomplete

§ Upper bound: Expansion gives an exponential-sizednondeterministic automaton § Lower bound: Can guess the error in the encoding of computation of expspace Turing machine, and count succinctly § Recall: for pushdown automata, emptiness is in P, but emptiness of intersection and universality are undecidable

Concurrent Hierarchical Automata
q Concurrency (synchronization on common symbols) and hierarchy nested. A component is
§ parallel compositionof already defined components, or § Hierarchical state machine with nodes and boxes, with boxes mapped to already defined components

qIf each hierarchical component has k nodes/boxes, a parallel component has at most d components, and nesting depth is m, then expansion has size O(k d^m) qReachability is expspace-complete qUniversality is 2expspace-complete

Reachability Summary
What is thecost of concurrency and hierarchy ? FSM : NLogSpace

Concurrent : PSPACE

Hierarchical: PTIME

Concurrent Hierarchical: EXPSPACE

Succinctness
q Standard automata: NFA are exp succinct than DFA (consider {w | exists i. wi=wn+i } ) q NFA are exp more succinct than DHA (det hierarchical) for same reason q DHA exp more succinct than NFA (consider {w#wR | |w|=n} ) q NHA (nondethierarchical) are doubly-exp more succinct than DHA/DFA (consider { w | exists i. wi = w i+2n } ) q Concurrent hierarchical automata are doubly-exp succinct than NHA/NFA and triply-more succinct than DFA/DHA (consider {w0#w1#… | exists i. wi=wj and |wi|=2n} )

Succinctness Summary
C+H+N Features: N: Nondeterminism H: Hierarchy C: Concurrency 3exp H exp 2exp 2exp exp exp DFAs H+N exp N exp

Talk...