Decidability Results for Well-Structured Transition Systems with Auxiliary Storage

Abstract. We consider the problem of verifying the safety of wellstructured transition systems (WSTS) with auxiliary storage. WSTSs with storage are automata that have (possibly) infinitely many control states along with an auxiliary store, but which have a well-quasi-ordering on the set of control states. The set of reachable configurations of the automaton may themselves not be well-quasi-ordered because of the presence of the extra store. We consider the coverability problem for such systems, which asks if it is possible to reach a control state (with some store value) that covers some given control state. Our main result shows that if control state reachability is decidable for automata with some store and finitely many control states then the coverability problem can be decided for WSTSs (with infinitely many control states) and the same store, provided the ordering on the control states has some special property. The special property we require is defined in terms of the existenc...

• Type: Conference
• Year: 2007
• Where: CONCUR
• Authors: Rohit Chadha, Mahesh Viswanathan
• Keywords: Auxiliary Storage, CONCUR 2007, Control States, Coverability Problem, Distributed And Parallel Computing