Title: State Space Reduction for Reachability Graph of CSM Automata,
Abstract: 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.