Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
5 results

Model Checking Vector Addition Systems with one zero-test

Rémi Bonnet ; Alain FInkel ; Jérôme Leroux ; Marc Zeitoun.
We design a variation of the Karp-Miller algorithm to compute, in a forward manner, a finite representation of the cover (i.e., the downward closure of the reachability set) of a vector addition system with one zero-test. This algorithm yields decision procedures for several problems for these&nbsp;[&hellip;]
Published on June 19, 2012
Volume 8, Issue 2

Forward Analysis for WSTS, Part II: Complete WSTS

Alain Finkel ; Jean Goubault-Larrecq.
We describe a simple, conceptual forward analysis procedure for infinity-complete WSTS S. This computes the so-called clover of a state. When S is the completion of a WSTS X, the clover in S is a finite description of the downward closure of the reachability set. We show that such completions are&nbsp;[&hellip;]
Published on September 29, 2012
Volume 8, Issue 3

Forward Analysis for WSTS, Part III: Karp-Miller Trees

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&nbsp;[&hellip;]
Published on June 23, 2020
Volume 16, Issue 2

Verification of Flat FIFO Systems

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&nbsp;[&hellip;]
Published on October 14, 2020
Volume 16, Issue 4

Branch-Well-Structured Transition Systems and Extensions

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&nbsp;[&hellip;]
Published on June 12, 2024
Volume 20, Issue 2
  • < Previous
  • 1
  • Next >