Liveness of Randomised Parameterised Systems under Arbitrary Schedulers

被引:12
|
作者
Lin, Anthony W. [1 ]
Rummer, Philipp [2 ]
机构
[1] Yale NUS Coll, Singapore, Singapore
[2] Uppsala Univ, Uppsala, Sweden
来源
COMPUTER AIDED VERIFICATION: 28TH INTERNATIONAL CONFERENCE, CAV 2016, PT II | 2016年 / 9780卷
关键词
MODEL CHECKING; PROBABILISTIC TERMINATION; REACHABILITY ANALYSIS; VERIFICATION; INFINITE; TOOL; TRANSDUCERS; AUTOMATA;
D O I
10.1007/978-3-319-41540-6_7
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:112 / 133
页数:22
相关论文
共 50 条
  • [31] On the refinement of liveness properties of distributed systems
    Attie, Paul C.
    FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (01) : 1 - 46
  • [32] Typing Liveness in Multiparty Communicating Systems
    Padovani, Luca
    Vasconcelos, Vasco Thudichum
    Vieira, Hugo Torres
    COORDINATION MODELS AND LANGUAGES, COORDINATION 2014, 2014, 8459 : 147 - 162
  • [33] Liveness characterization for GFC systems (I)
    Sci China Ser E Technol Sci, 2 (196):
  • [34] Propositional Gossip Protocols under Fair Schedulers
    Livesey, Joseph
    Wojtczak, Dominik
    PROCEEDINGS OF THE THIRTY-FIRST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, IJCAI 2022, 2022, : 391 - 397
  • [35] Verification of Liveness Properties in Distributed Systems
    Yadav, Divakar
    Butler, Michael
    CONTEMPORARY COMPUTING, PROCEEDINGS, 2009, 40 : 625 - +
  • [36] Using schedulers to test probabilistic distributed systems
    Hierons, Robert M.
    Nunez, Manuel
    FORMAL ASPECTS OF COMPUTING, 2012, 24 (4-6) : 679 - 699
  • [37] A generic approach for the automatic verification of featured, parameterised systems
    Miller, A
    Calder, M
    FEATURE INTERACTIONS IN TELECOMMUNICATIONS AND SOFTWARE SYSTEMS VIII, 2005, : 217 - 235
  • [38] On the refinement of liveness properties of distributed systems
    Paul C. Attie
    Formal Methods in System Design, 2011, 39 : 1 - 46
  • [39] Static Analysis Techniques for Parameterised Boolean Equation Systems
    Orzan, Simona
    Wesselink, Wieger
    Willemse, Tim A. C.
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2009, 5505 : 230 - 245
  • [40] Verification of reactive systems via instantiation of Parameterised Boolean Equation Systems
    Ploeger, B.
    Wesselink, J. W.
    Willemse, T. A. C.
    INFORMATION AND COMPUTATION, 2011, 209 (04) : 637 - 663