时间行为协议状态空间约减算法

对复杂时间行为协议状态进行约减对于缓解形式化验证的状态空间爆炸问题，提高验证工具系统的效率、实用性等具有重要意义。分析了实时构件组合的几种形态，对基于时间行为协议的组合理论和状态空间爆炸问题进行了讨论，给出了时间行为协议的状态空间约减算法并进行了分析，给出了示例。