FIFO systems are systems of automata communicating through FIFO queues. This simple and rather idealised model can be used to analyse some aspects of message-passing systems, reactive systems with event queues, weak memory models with buffered reads and writes, etc. From
a purely computational perspective, this is a Turing complete model even for just one automaton and one FIFO queue.
In this talk, I will present a personal selection of existing works on the problem of the automatic (push-button) verification of such systems. I will consider in particular the works that try to address the verification of FIFO systems that are "nearly" systems with rendez-vous synchronisation.
Nearly synchronous FIFO systems can be found for instance in the work of Lipton on reduction [1], Elrad&Francez on communication closed layers [2],
Bultan et al on synchronisability [3], Mushcoll et al on existential boundedness [4], or more recently Bouajjani et al on k-synchronous systems [5].
This idea is also implicitly present in several works on multi-party session types [6], although the connection there is only well understood in the bipartite setting, where it matches the notion of half-duplex communications [7,8]. The aim of the talk will also be to present recent personal contributions and ongoing works on k-synchronous systems, existentially-bounded systems, and half-duplex systems [9,10,11,12].

[1] Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Commun. ACM 18(12), 717–721 (1975).https://doi.org/10.1145/361227.361234

[2] Elrad, T., Francez, N.: Decomposition of distributed programs into communication-closed layers. Sci. Comput. Program. 2(3), 155–173 (1982).https://doi.org/10.1016/0167-6423(83)90013-8

[3] Basu, S., Bultan, T.: On deciding synchronizability for asynchronously communicating systems. Theor. Comput. Sci.https://doi.org/10.1016/j.tcs.2016.09.023