University of Illinois Urbana-Champaign

Decidability Results for Well-Structured Transition Systems with Auxiliary Storage

Chadha, Rohit; Viswanathan, Mahesh

Content Files
Decidability Results for Well-Structured Transition Systems with Auxiliary Storage.pdf

Permalink

https://hdl.handle.net/2142/11342

Description

Title
Decidability Results for Well-Structured Transition Systems with Auxiliary Storage
Author(s)
  • Chadha, Rohit
  • Viswanathan, Mahesh
Issue Date
2007-06
Keyword(s)
computer science
Date of Ingest
2009-04-22T15:22:16Z
Abstract
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 {\it 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.
Type of Resource
text
Genre of Resource
Technical Report
Permalink
http://hdl.handle.net/2142/11342
Copyright and License Information
You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections

Research and Tech Reports - Computer Science PRIMARY