Liveness of Randomised
Parameterised Systems
under Arbitrary Schedulers
Anthony W. Lin and Philipp Ruemmer

Summary of results•

Automatic method for proving liveness for
randomised parameterised systems, e.g.,•Randomised Self-Stabilising (Israeli-Jalfon/Herman)•

Randomised Dining Philosopher (Lehmann-Rabin)•

Regular model checking as symbolic framework•CEGAR/Learning to synthesise “regular proofs”

BackgroundParameterised Systems
Definition: An infinite family of finite-state systems
Example: most distributed protocols in the verification
literature, e.g., for the Dining Philosopher problem

Randomised Parameterised
Systems
Definition: An infinite family of randomised
finite-state systems
Markov Decision Processes
1/2
1/2
1/2
1/21

Israeli-Jalfon Randomised
Self-Stabilising Protocol
1/2
1/2Israeli-Jalfon Randomised
Self-Stabilising Protocol
1/2
1/2Israeli-Jalfon Randomised
Self-Stabilising Protocol

Israeli-Jalfon Randomised
Self-Stabilising Protocol
1/2
1/2Israeli-Jalfon Randomised
Self-Stabilising Protocol

Israeli-Jalfon Randomised
Self-Stabilising Protocol

Israeli-Jalfon Randomised
Self-Stabilising Protocol

Liveness (a.k.a. almost-suretermination)(1) Can be unfair(2) Desirable property in
self-stabilising protocolliterature

Liveness for Parameterised
Systems•

Infinite-state verification (verify for each instance)•

Challenging esp. for probabilitistic systems, e.g.,•

Randomised Self-Stabilising (Israeli-Jalfon/Herman)•

Randomised Dining Philosopher (Lehmann-Rabin)reachability games on infinite graphs

Regular Model Checking:Symbolic Framework

Regular Specification“Rich language for specifying parameterised systems
using automata”
Pioneered by:* Kesten, Maler, Marcus, Pnueli, and Shahar (1997)* Wolper and Boigelot (1998)* Jonsson and Nilsson (2000)* Bouajjani, Jonsson, Nilsson, and Touili (2000)

Premier of regularspecifications
Configuration: represented as a word
Set of configurations: represented as a regular automaton
Transition relation: represented as a transducer

Length-preservingIsraeli-Jalfon as a regularspecification
Configuration: a word over the alphabet {0,1,1}

10001

Israeli-Jalfon as a regularspecification
Configuration: a word over the alphabet {0,1,1}

10001Israeli-Jalfon as a regularspecification
Set of configurations: a regular language over {0,1,1}
All stable configurations
0*10*

All initial configurations
1+

Israeli-Jalfon as a regularspecification
Nondeterministic transition relation: a regular language
over {0,1} x {0,1,1}

10001
10001

Israeli-Jalfon as a regularspecification
Nondeterministic transition relation: a regular language
over {0,1} x {0,1,1}

10001
10001

Israeli-Jalfon as a regularspecification
Nondeterministic transition relation: a regular language
over {0,1} x {0,1,1}10001
10001

Israeli-Jalfon as a regularspecification
Nondeterministic transition relation: a regular language
over {0,1} x {0,1,1}

10001
10001

Israeli-Jalfon as a regularspecification
Nondeterministic transition relation: a regular language
over {0,1} x {0,1,1}

10001
10001

L =

01+01

*

1
1

01+01

*

Israeli-Jalfon as a regularspecification
Problem: How do you represent probabilistictransitions as transducers?
Answer: almost sure liveness for finite MDPs, need only
distinguish zero or non-zero probabilities
Proposition (Hart et al.’83): almost sure liveness =2-player non-stochastic reachability games
Generalises to infinite family of finite MDPs (why?)Israeli-Jalfon as a regularspecification
Probabilistic transition relation: a regular language over{0,1,1} x {0,1}
01+0
10
1+0
1

*

*

10
1
00
1
1
101+0
10
1+01

*

*

Pass to right(w/o Mars bar)
Pass to right(with Mars bar)………. (~10 more cases)

Semi-decision procedure
Proposition (Hart et al.’83): almost sure liveness =wins non-stochastic reachability games
from each reachable state.
1/2
1/2
1/2
1/21Semi-decision procedure
Prop (LR’16): ’s winning strategies can be
represented as “advice bits”

Inductive invariant

Well-founded relationthat guides to winSemi-decision procedure•

Advice bits

are infinite objects•

Solution: represent
by an automaton andby a transducer (“regular advice bits”)
Prop: There exists a complete algorithm
for verifying regular advice bits

Regular advice bits often exist in practiceRegular advice bits for
Israeli-Jalfon
1u010/01/10
0/1

0

0/0
0/1
30/0
1/0
1/1

0/0
0/1
1/1
1/1
1/0

1/0
1

0/12

Learning Regular
Advice Bits

Problem
Although regular advice bits exist, a naive
enumeration might take a long time to find them

Our monolithic learning
procedure
Teacher

Learner
Regularadvice bits?
NO(cex)YESDONE

Inside the learner
SAT-solving to guess smallest DFAs
Boolean formulas constraining candidate
regular advice bits

Inside the teacher
Automata-based algorithm
If incorrect advice bits,
return cex(as a boolean formula)The learner then …
Add the counterexample constraint
from Teacher to further restrict
And make another guess, etc.

The main bottleneck
The number of iterations~
The number of candidate regular advice bits considered

Each iteration is quite cheap

Further optimisations
Problem: When no “small” regular proof exists,monolithic procedure becomes very slow•

Incremental learning algorithm: use“disjunctive” advice bits•

Precomputation of inductive invariant with
Angluin’s L* algorithm•

Symmetries (e.g. rotations for rings)

Experiments(https://github.com/uuverifiers/ autosat/tree/master/LivenessProver)Experimental results

Experimental results

Conclusion

Summary of results•

Automatic method for proving liveness for
randomised parameterised systems, e.g.,•

Randomised Self-Stabilising (Israeli-Jalfon/Herman)•

Randomised Dining Philosopher (Lehmann-Rabin)•

Regular model checking as symbolic framework•

CEGAR/Learning to synthesise “regular proofs”

Future Work•

Embedding fairness in RMC••

New result (joint with O. Lengal, R. Majumdar)

Extend the framework to encode process IDs