Etienne Lozes

  Parikh finite automata as abstract domains for FIFO systems

       FIFO systems, or communicating finite state machines, are a computational model where letters can be queued and dequeued. Unlike for stack machines, a single queue is enough to yield undecidability. This makes the design of automatic techniques for the analysis of asynchronous protocols rather hard, and the known restrictions on the communication model that restore decidability do not encompass a large number of protocols. As a consequence, some works on FIFO systems also address the verification problem by means of acceleration, widdening, or CEGAR-like techniques, with some success on a collection of case studies.        Parikh finite automata have been introduced by Klaedke and Ruess for deciding MSO with cardinalities. They are a simple extension of finite state automata where the standard acceptance condition is strenghthened by an arithmetic constraint on the commutative image of the (run of the) word being recognized.            I will present an example protocol for which all known verification tecnhniques fail, and that suggests that PFA should be used as abstract domains to automate the verification. I am there mainly influenced by a work of Bouajjani and Habermehl, who introduced a restricted class of Parikh finite automata called CQDD, that they used to effectively compute the loop acceleration of FIFO systems, a problem first studied by Boigelot. I will present an extension of the result of Bouajjani and Habermehl for other forms of acceleration, and I will conclude on a discussion on implementation issues I am currently working on - which will show that, although theoretically appealing, the approach I present may not be the right one to follow in tool design. No preliminary knowledge of FIFO systems or Parikh automata is required.