CSM自动机可达图的状态空间约简
State Space Reduction for Reachability Graph of CSM Automata
摘要：
经典的CTL时态逻辑是建立在具有交错模型并发的系统上的。许多尝试是为了解决状态空间爆炸问题（例如，组合模型检验）。有一些基于动作独立性的状态空间缩减方法。然而，在CSM模型，这是基于重合而不是交错，动作的独立性不能定义。因此，提出了基于相同的时间后果，而不是独立的行动的状态空间约简。新的减少不如交织系统好，因为在减少之前必须获得状态的所有后继者（在两个级别的深度）。这导致状态空间的表示所需的空间的减少，但不是在状态空间构造的时间。然而，在CSM系统的常规状态空间中可能会发生很多节省。
英文摘要：
Classical CTL temporal logics are built over systems with interleaving model concurrency. Many attempts are made to fight a state space explosion problem (for instance, compositional model checking). There are some methods of reduction of a state space based on independence of actions. However, in CSM model, which is based on coincidences rather than on interleaving, independence of actions cannot be defined. Therefore a state space reduction basing on identical temporal consequences rather than on independence of action is proposed. The new reduction is not as good as for interleaving systems, because all successors of a state (in depth of two levels) must be obtained before a reduction may be applied. This leads to reduction of space required for representation of a state space, but not in time of state space construction. Yet much savings may occur in regular state spaces for CSM systems.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
