Verification of Succinct Hierarchical State Machines
Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato · ePrints Soton (University of Southampton) · 2007
A hierarchical state machine (HSM) is a finite state machine where a vertex can either expand to another hierarchical state machine (box) or be a basic vertex (node). Each node is labeled with atomic propositions. We study an extension of such model which allows atomic propositions to label also boxes (SHSM). We show that SHSMs can be exponentially more succinct than HSMs, and verification is in general harder by an exponential factor. Also, we show for a subclass of SHSMs (which can still be exponentially more succinct than HSMs) the same upper bounds as for HSMs.