TY - GEN

T1 - Decidability results for well-structured transition systems with auxiliary storage

AU - Chadha, R.

AU - Viswanathan, M.

PY - 2007

Y1 - 2007

N2 - We consider the problem of verifying the safety of well-structured 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 existence of a ranking function compatible with the transition relation. We then show that there are several classes of infinite state systems that can be viewed as WSTSs with an auxiliary storage. These observations can then be used to both reestablish old decidability results, as well as discover new ones.

AB - We consider the problem of verifying the safety of well-structured 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 existence of a ranking function compatible with the transition relation. We then show that there are several classes of infinite state systems that can be viewed as WSTSs with an auxiliary storage. These observations can then be used to both reestablish old decidability results, as well as discover new ones.

UR - http://www.scopus.com/inward/record.url?scp=38149068191&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=38149068191&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-74407-8_10

DO - 10.1007/978-3-540-74407-8_10

M3 - Conference contribution

AN - SCOPUS:38149068191

SN - 9783540744061

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 136

EP - 150

BT - CONCUR 2007 - Concurrency Theory - 18th International Conference, CONCUR 2007, Proceedings

PB - Springer

T2 - 18th International Conference on Concurrency Theory, CONCUR 2007

Y2 - 3 September 2007 through 8 September 2007

ER -