Well-structured pushdown systems
Intervenant(s) : Mizuhito Ogawa (JAIST, Kanazawa)
Well-structured pushdown systems (WSPDS) is an extension of Well-structured transition systems (WSTS) with a single stack. We show general conditions for decidability of coverability of WSPDS. Various VASS extensions (RVASS, BVAS, VASS with one-zero test) are examples of the forward technique, and Dense timed pushdown automata and Nested Timed Automata are those of the backward technique.
We also discuss on related work, like VASS with inhibition, interrupt timed automata (ITA), and another recent WSPDS result by Jerome Leroux.