Actively learning to verify safety for FIFO automata

Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha

Research output: Contribution to journalArticle

Abstract

We apply machine learning techniques to verify safety properties of finite state machines which communicate over unbounded FIFO channels. Instead of attempting to iteratively compute the reachable states, we use Angluin's L* algorithm to learn these states symbolically as a regular language. The learnt set of reachable states is then used either to prove that the system is safe, or to produce a valid execution of the system that leads to an unsafe state (i.e. to produce a counterexample). Specifically, we assume that we are given a model of the system and we provide a novel procedure which answers both membership and equivalence queries for a representation of the reachable states. We define a new encoding scheme for representing reachable states and their witness execution; this enables the learning algorithm to analyze a larger class of FIFO systems automatically than a naive encoding would allow. We show the upper bounds on the running time and space for our method. We have implemented our approach in Java, and we demonstrate its application to a few case studies.

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Actively learning to verify safety for FIFO automata'. Together they form a unique fingerprint.

  • Cite this