Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
4 results

Well Behaved Transition Systems

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&nbsp;[&hellip;]
Published on September 13, 2017
Volume 13, 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

Synchronizability of Communicating Finite State Machines is not Decidable

Alain Finkel ; Etienne Lozes.
A system of communicating finite state machines is synchronizable if its send trace semantics, i.e.the set of sequences of sendings it can perform, is the same when its communications are FIFO asynchronous and when they are just rendez-vous synchronizations. This property was claimed to be decidable&nbsp;[&hellip;]
Published on December 20, 2023
Volume 19, Issue 4
  • < Previous
  • 1
  • Next >