Modular verification of modular finite state machines

This paper summarizes the key results for modular verification of modular finite state machines; that is, for verifying the correctness of a system of modular finite state machines without performing the composition of all of the modules. The modular finite state machine framework is first reviewed; this framework differs from standard finite state machines in that there are two types of events: triggers, which the system reacts to, and responses, which it generates or forces to occur. Because the proofs of modular verification are based on the languages generated by modular finite state machines, the main definitions and properties of trigger response languages are summarized. The paper also describes the computational complexity of the modular verification procedure.