本发明公开一种层次式时间自动机平展化算法，步骤是：（1）针对层次式时间自动机中的每一个非根顺序时间自动机，相应地添加inactive状态；（2）针对每个非根节点顺序时间自动机，添加一个特殊状态，并从源于复合状态的转移的相应的源限制函数值中的每个状态添加相应的转移到该特殊状态，并将该转移对应的事件扩充为广播通道类型,并将上面到达新状态的转移事件扩充为该广播通道类型的接受类型；（3）从步骤（2）每个顺序时间自动机中新添加的特殊状态出发引出新的转移，到达步骤（1）中所添加的对应的顺序时间自动机中的inactive状态。此种算法可使得平展后的结果能够作为模型检测工具的输入，从而进行自动化的验证。