4 results
Michael Blondin ; Alain Finkel ; Jean Goubault-Larrecq.
This paper is a sequel of "Forward Analysis for WSTS, Part I: Completions" [STACS 2009, LZI Intl. Proc. in Informatics 3, 433-444] and "Forward Analysis for WSTS, Part II: Complete WSTS" [Logical Methods in Computer Science 8(3), 2012]. In these two papers, we provided a framework to conduct forward […]
Published on June 23, 2020
Alain Finkel ; M. Praveen.
The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by […]
Published on October 14, 2020
Michael Blondin ; Alain Finkel ; Pierre McKenzie.
The well-quasi-ordering (i.e., a well-founded quasi-ordering such that all antichains are finite) that defines well-structured transition systems (WSTS) is shown not to be the weakest hypothesis that implies decidability of the coverability problem. We show coverability decidable for monotone […]
Published on September 13, 2017
Benedikt Bollig ; Alain Finkel ; Amrita Suresh.
We propose a relaxation to the definition of well-structured transition systems (\WSTS) while retaining the decidability of boundedness and non-termination. In this class, the well-quasi-ordered (wqo) condition is relaxed such that it is applicable only between states that are reachable one from […]
Published on June 12, 2024