Sciweavers

Share
CONCUR
2007
Springer

Decidability Results for Well-Structured Transition Systems with Auxiliary Storage

10 years 3 months ago
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...
Rohit Chadha, Mahesh Viswanathan
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where CONCUR
Authors Rohit Chadha, Mahesh Viswanathan
Comments (0)
books