随机参数化系统在任意扰动下的活性（技术报告）
Liveness of Randomised Parameterised Systems under Arbitrary Schedulers (Technical Report)
摘要：
我们考虑的问题，验证系统的活性有限，但无界，过程的数量，通常被称为参数化系统。这类系统的典型例子包括分布式协议（例如哲学家就餐问题）。与验证安全性的情况不同，证明活性仍然被认为是极具挑战性的，特别是在系统中存在随机性的情况下。在本文中，我们考虑任意（包括不公平的）干扰下的活性，这通常被认为是一个理想的属性在文学的自稳定系统。我们介绍了一种自动的方法证明活性的随机参数化系统在任意的干扰。将活性视为两个玩家之间的可达性游戏（在过程和过程之间），我们的方法是CEGAR方法，该方法合成了过程的进度关系，该过程可以象征性地表示为有限状态自动机。该方法是增量的，并利用了Angluin风格的L* 学习和SAT求解器。我们的实验表明，我们的算法能够自动证明著名的随机分布式协议，包括莱曼拉宾随机用餐哲学家协议和随机自稳定协议（如以色列Jalfon协议）的活性。据我们所知，这是第一个可以证明随机协议活性的全自动方法。
英文摘要：
We consider the problem of verifying liveness for systems with a finite, but unbounded, number of processes, commonly known as parameterised systems. Typical examples of such systems include distributed protocols (e.g. for the dining philosopher problem). Unlike the case of verifying safety, proving liveness is still considered extremely challenging, especially in the presence of randomness in the system. In this paper we consider liveness under arbitrary (including unfair) schedulers, which is often considered a desirable property in the literature of self-stabilising systems. We introduce an automatic method of proving liveness for randomised parameterised systems under arbitrary schedulers. Viewing liveness as a two-player reachability game (between Scheduler and Process), our method is a CEGAR approach that synthesises a progress relation for Process that can be symbolically represented as a finite-state automaton. The method is incremental and exploits both Angluin-style L*-learning and SAT-solvers. Our experiments show that our algorithm is able to prove liveness automatically for well-known randomised distributed protocols, including Lehmann-Rabin Randomised Dining Philosopher Protocol and randomised self-stabilising protocols (such as the Israeli-Jalfon Protocol). To the best of our knowledge, this is the first fully-automatic method that can prove liveness for randomised protocols.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
