Abstract
Most decidability results concerning well-structured transition systems apply to the finitely branching variant. Yet some models (inserting automata, ω-Petri nets, ...) are naturally infinitely branching. Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are finite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the control-state maintainability and the coverability problems. Coverability and boundedness under new effectivity conditions are shown decidable. © 2014 Springer-Verlag.
Cite
CITATION STYLE
Blondin, M., Finkel, A., & McKenzie, P. (2014). Handling infinitely branching WSTS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8573 LNCS, pp. 13–25). Springer Verlag. https://doi.org/10.1007/978-3-662-43951-7_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
