2017/10/25 by Wiktor B. Daszczuk, Daszczuk, Wiktor B.
Computer Science · #68N30 #D.2.2 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques #Software Engineering (cs.SE) #acm:68N30 #cs.FL #cs.LO #cs.SE #msc:68N30
paper · pdf · doi:10.48550/arxiv.1710.09083
12 pages, 10 figures
arxiv created 2017/10/25 · openalex publication_date 2017/10/25 · arxiv updated 2017/10/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.