Information and Computation Paper - Case Studies

Included below are the models and properties used for running examples and to generate experimental results in the paper:

• "Compositional Probabilistic Verification through Multi-Objective Model Checking"
  by Marta Kwiatkowska, Gethin Norman, David Parker and Hongyang Qu.

Running examples

• Example 2: model and properties
• Example 3: model and properties
• Examples 4, 6, 7 and 8: model and properties
• Example 5: model and properties

Randomised consensus [AH90]

1. The minimum probability that the processes decide by round R;

   This property can be represented by a probabilistic safety property. We use the rule (Asym-Safety), in conjunction with the rule (Async-Safety) to establish the required assumptions.

   • Two processes

     • Probabilistic safety property used in the (Async-Safety) rule application: model and property
     • multi-objective query from the (Asym-Safety) rule application (3 rounds): model and property
     • multi-objective query from the (Asym-Safety) rule application (4 rounds): model and property
     • multi-objective query from the (Asym-Safety) rule application (5 rounds): model and property
     • Non-compositional model checking: model (3 rounds, 4 rounds and 5 rounds) and property

   • Three processes

     • Probabilistic safety property used in the (Async-Safety) rule application: model and property
     • multi-objective query from the (Asym-Safety) rule application (3 rounds): model and property
     • multi-objective query from the (Asym-Safety) rule application (4 rounds): model and property
     • Non-compositional model checking: model (3 rounds and 4 rounds) and property
   
   
   
2. The maximum expected number of steps required in the first R rounds.

   Compositional verification of this property is performed by first splitting the reward structure for the property into several parts (one for the N processes and one for each coin protocol) and then using rule (Async-Quant) to determine an upper bound on the maximum total expected value for each one. Then combining these results, using the (Sum-Reward) rule, to compute an upper bound on the maximum total reward.

   • Two processes

     • Assumptions on coin protocols uses (Async-Quant) rule (standard probabilistic model checking):
       • probability coin protocol returns same value for all processes: model and property
         
         
     • Assumptions on processes uses (Async-Quant) rule (assumes probabilistic property of coin protocols):
       • probability coin protocol of the second round is invoked: model and property
       • probability coin protocol of the third round is invoked: model and property
         
         
     • Guarantees on process uses (Async-Quant) rule (assumes properties of coin protocols):
       • maximum expected reward for processes (3 rounds): model and property
       • maximum expected reward for processes (4 rounds): model and property
       • maximum expected reward for processes (5 rounds): model and property
         
         
     • Guarantees on coin protocols uses (Async-Quant) rule (assumes properties of processes):
       • maximum expected reward for coin protocol of round 1: model and property
       • maximum expected reward for coin protocol of round 2: model and property
       • maximum expected reward for coin protocol of round 3: model and property
         
         
     • Non-compositional model checking: model (3 rounds, 4 rounds and 5 rounds) and property
       
       

   • Three processes

     • Assumptions on coin protocols (standard probabilistic model checking):
       • probability coin protocol returns same value for all processes: model and property
         
         
     • Assumptions on processes uses (Async-Quant) rule (assumes probabilistic property of coin protocols):
       • probability coin protocol of the second round is invoked: model and property
         
         
     • Guarantees on process uses (Async-Quant) rule (assumes properties of coin protocols):
       • maximum expected reward for processes (3 rounds): model and property
       • maximum expected reward for processes (4 rounds): model and property
         
         
     • Guarantees on coin protocols uses (Async-Quant) rule (assumes properties of processes):
       • maximum expected reward for coin protocol of round 1: model and property
       • maximum expected reward for coin protocol of round 2: model and property
         
         
     • Non-compositional model checking: model (3 rounds, 4 rounds) and property
       
       

Zeroconf network configuration protocol [CAG02] (PA model from [KNPS06])

1. Minimum probability that a host only employs a fresh IP address.
2. Minimum probability that a host is configured by time T.

   These two properties are probabilistic both safety properties, which are verified compositionally by first applying the rule (Circ-Safety), where the first and second assumptions concern the new host and environment, respectively, and the first assumption is a qualitative (probability 1) safety property.

   • Assumption on host (qualitative safety property): model and property
     
     
   • Assumptions on environment (assumes properties on host encoded as a automaton as qualitative assumption): model (K=2, K=4, K=6 and K=8) and property
     
     
   • Guarantees on the host (assumes properties on environment):
     • Minimum probability that a host only employs a fresh IP address: model (K=2, K=4, K=6 and K=8) and property.
     • Minimum probability that a host is configured by time T: model (K=2 and K=4) and property
     
     
   • Non-compositional model checking:
     • Minimum probability that a host only employs a fresh IP address: model and property
     • Minimum probability that a host is configured by time T:model and property
   
   
   
3. Minimum probability that the protocol terminates.
4. Minimum and maximum expected time for the protocol to terminate.

   For these properties verification is performed by first applying the rule (Circ-Safe), where the first assumption is a either a qualitative safety or qualitative liveness property, about the new host, and the second assumption is a probabilistic omega-regular property, concerning the environment.

   • Assumptions on host (standard probabilistic model checking):
     • safety assumptions on the host (encoded with automata): model and property
     • actions send1 and send2 performed only finitely many time: model and property
       
       
   • Assumptions on environment (assumes properties on host):
     • actions rec0 and rec1 performed only finitely many time: model and property
       
       
   • Guarantees on the host (assumes properties on environment):
     • liveness (minimum probability host configures): model and property
     • minimum expected time to configure: model and property
     • maximum expected time to configure: model and property
       
       
   • Non-compositional model checking: model and property