English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Tools annual

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools monthly

Global: Zendy Plus monthly

Presents the access of premium content as premium feature

Premium Content

Global: Zendy Plus annual

Global: Zendy Free Plan

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

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