This page provides some supplementary information of our work on Assume-Guarantee Abstraction Refinement (AGAR) for Probabilistic Systems, modeled as Labeled Probabilistic Transition Systems (LPTSes). Technical details of this work can be found in our CAV 2012 paper.

We use the following two compositional rules, ASym and ASym-N where L_i’s, A and P are LPTSes.

Our prototype tool can be downloaded here.

We evaluated AGAR for these rules on the following examples, taken from previous work. For each example, the PRISM model files (extension .nm) for the components and specifications are given for the largest parameter. Links to files of other parameters are also given at the end.

Each model file is associated with a text file enumerating the alphabet (extension .acts) of the corresponding LPTS, each action appearing in a new line and an empty line indicating an internal (tau) action. L denotes the whole system obtained by composing all the components.

1. 1. Client-Server with 1 failure (7 clients)
   

2. L : cs.nm, cs.acts
   

3. P : spec.nm, spec.acts
   

1. ASym
   

2. L1 : server.nm, server.acts
   

3. L2 : clients.nm, clients.acts
   

1. ASym-N
   

2. L1 : server.nm, server.acts
   

3. L2 : client1.nm, client1.acts
   

4. L3 : client2.nm, client2.acts
   

5. L4 : client3.nm, client3.acts
   

6. L5 : client4.nm, client4.acts
   

7. L6 : client5.nm, client5.acts
   

8. L7 : client6.nm, client6.acts
   

9. L8 : client7.nm, client7.acts
   

1. Parameter 5     Parameter 6
   

2. 2. Client-Server with N failures (4 clients)
   

3. L : cs.nm, cs.acts
   

4. P : spec.nm, spec.acts
   

1. ASym
   

2. L1 : clients.nm, clients.acts
   

3. L2 : server.nm, server.acts
   

1. ASym-N
   

2. L1 : server.nm, server.acts
   

3. L2 : client1.nm, client1.acts
   

4. L3 : client2.nm, client2.acts
   

5. L4 : client3.nm, client3.acts
   

6. L5 : client4.nm, client4.acts
   

1. Parameter 2     Parameter 3
   

3. 3. Mars Exploration Rovers (5 users)
   

4. L : mer.nm, mer.acts
   

5. P : spec.nm, spec.acts
   

1. ASym
   

2. L1 : arbiter.nm, arbiter.acts
   

3. L2 : users.nm, users.acts
   

1. ASym-N
   

2. L1 : arbiter.nm, arbiter.acts
   

3. L2 : user1.nm, user1.acts
   

4. L3 : user2.nm, user2.acts
   

5. L4 : user3.nm, user3.acts
   

6. L5 : user4.nm, user4.acts
   

7. L6 : user5.nm, user5.acts
   

1. Parameter 3     Parameter 4
   

4. 4. Sensor Network (3 sensors)
   

5. L : sn.nm, sn.acts
   

6. P : spec.nm, spec.acts
   

1. ASym
   

2. L1 : non_proc.nm, non_proc.acts
   

3. L2 : proc.nm, proc.acts
   

1. ASym-N
   

2. L1 : channel.nm, channel.acts
   

3. L2 : proc.nm, proc.acts
   

4. L3 : sensor1.nm, sensor1.acts
   

5. L4 : sensor2.nm, sensor2.acts
   

6. L5 : sensor3.nm, sensor3.acts
   

1. Parameter 1     Parameter 2