2018/03/06 by Vasumathi K. Narayanan, Narayanan, Vasumathi K.
Computer Science · #Cognitive Computing and Networks #Computability, Logic, AI Algorithms #Distributed systems and fault tolerance #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Multiagent Systems (cs.MA) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1803.03127
openalex publication_date 2018/03/06 · openalex created_date 2022/10/03 · openalex updated_date 2026/07/28
In this work, we alleviate the well-known State-Space Explosion (SSE) problem\nin Component Based Systems (CBS). We consider CBS that can be specified as a\nsystem of n Communicating Finite State Machines (CFSMs) interacting by\nrendezvous/handshake method. In order to avoid the SSE incurred by the\ntraditional product machine composition of the given input CFSMs based on\ninterleaving semantics, we construct a sum machine composition based on\nstate-oriented partial-order semantics. The sum machine consists of a set of n\nunfolded CFSMs. By storing statically, just a small subset of global state\nvectors at synchronization points, called the synchronous environment vectors\nand generating the rest of the global-state vectors dynamically on need basis\ndepending on the reachability to be verified, the sum machine alleviates the\nSSE of the product machine. We demonstrate the implementation of checking the\nreachability of global state vector from the checking of local reachabilities\nof the components of the given state vector, through a parallel, distributed\nalgorithm. Parallel and distributed algorithms to generate the sum machine and\nverifying the reachability in it both without exponential complexity are the\ncontributions of this work. Keywords: interleaving semantics, partial-order\nsemantics, sum machine, product machine, synchronization points, synchronous\nenvironment state vectors, reachability.\n