Space Efficient Methods for Testing Reachability with Applications to Coobservability and Decentralized Control

All known methods of deciding coobservability use exponential space and we demonstrate that we can decide coobservability using polynomial space. Coobservability is one of the necessary and sufficient conditions for deciding decentralized controller existence. Our method for deciding coobservability is based on a deterministic space efficient method we introduce for deciding state reachability for finite state systems. This reachability decision method runs in space O(q^2) where q is the size of the encoding of a system state. This memory bound allows us to decide reachability in large state space systems in a manner that avoids space constraints caused by the state explosion problem. However, there is a space-time tradeoff and our methods are potentially expensive in computation time. We discuss some experimental results that demonstrate this new method of deciding coobservability is more space efficient than the current known method but the time-space tradeoff causes these algorithms to be very inefficient in time.