Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
3 results

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

Bounded Reachability Problems are Decidable in FIFO Machines

Benedikt Bollig ; Alain Finkel ; Amrita Suresh.
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular&nbsp;[&hellip;]
Published on January 20, 2022
Volume 18, Issue 1
  • < Previous
  • 1
  • Next >