Learning to Prove Safety over Parameterised Concurrent Systems (Full Version)

TL;DR

This paper introduces a simple method using Angluin's L* algorithm to synthesize regular inductive invariants for parameterised concurrent systems, providing a termination guarantee and demonstrating competitive performance in safety verification tasks.

Contribution

It presents a novel, straightforward approach leveraging L* algorithm for safety proof in parameterised systems with a proven termination condition.

Findings

Method successfully synthesizes inductive invariants for various protocols.

Algorithm performs comparably to existing semi-algorithms in experiments.

Guarantees termination when the reachable set is regular.

Abstract

We revisit the classic problem of proving safety over parameterised concurrent systems, i.e., an infinite family of finite-state concurrent systems that are represented by some finite (symbolic) means. An example of such an infinite family is a dining philosopher protocol with any number n of processes (n being the parameter that defines the infinite family). Regular model checking is a well-known generic framework for modelling parameterised concurrent systems, where an infinite set of configurations (resp. transitions) is represented by a regular set (resp. regular transducer). Although verifying safety properties in the regular model checking framework is undecidable in general, many sophisticated semi-algorithms have been developed in the past fifteen years that can successfully prove safety in many practical instances. In this paper, we propose a simple solution to synthesise regular inductive invariants that makes use of Angluin's classic L* algorithm (and its variants). We provide a termination guarantee when the set of configurations reachable from a given set of initial configurations is regular. We have tested L* algorithm on standard (as well as new) examples in regular model checking including the dining philosopher protocol, the dining cryptographer protocol, and several mutual exclusion protocols (e.g. Bakery, Burns, Szymanski, and German). Our experiments show that, despite the simplicity of our solution, it can perform at least as well as existing semi-algorithms.