Abstract | ||
---|---|---|
Most decidability results concerning well-structured transition systems apply to the finitely branching variant. Yet some models (inserting automata, omega-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. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/978-3-662-43951-7_2 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Discrete mathematics,Forward algorithm,Computer science,Automaton,Decidability,Maintainability,Branching (version control) | Conference | 8573 |
ISSN | Citations | PageRank |
0302-9743 | 3 | 0.41 |
References | Authors | |
28 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Michael Blondin | 1 | 27 | 9.06 |
Alain Finkel | 2 | 26 | 3.30 |
Pierre McKenzie | 3 | 188 | 15.94 |