The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
We consider the problem of verifying the safety of well-uctured 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 tomaton may themselves not be well-quasi-ordered because of the presence of the extra store. consider the coverability problem for such systems, which asks if it is possible to reach a ntrol state (with some store value) that covers some given control state. Our main result that if control state reachability is decidable for automata with some store and finitely control states then the coverability problem can be decided for WSTSs (with infinitely many ntrol 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 ction compatible with the transition relation. We then show that there are several classes of nfinite state systems that can be viewed as WSTSs with an auxiliary storage. These can then be used to both reestablish old decidability results, as well as discover new ones.
Joint work with Mahesh Viswanathan.