Path Robustness: Grid-World Planning (NuSMV)

Description of the Case Study

Beyond optimality, we study path robustness for the same grid-world robot controller [NWP19]. The question is whether a single strategy can guide the robot to the goal from any admissible initial configuration. The HyperLTL formulation requires all runs that follow the synthesised strategy to synchronise on the same control choices, guaranteeing that every starting state eventually reaches the goal under that policy. HyperQB establishes SAT for grids up to \(60 \times 60\), showing that a uniform, robust controller exists even as the environment scales.

The NuSMV model(s)

Grid 10x10 (100 cells)Grid 20x20 (400 cells)Grid 40x40 (1,600 cells)Grid 60x60 (3,600 cells)

--(adopted from: Yu Wang, Siddharta Nalluri, and Miroslav Pajic. Hyperproperties for robotics: Planning via HyperLTL. In 2020 IEEE Int’l Conf. on Robotics and Automation (ICRA’20))
 MODULE main
 VAR
    x_axis: 0..9;
    y_axis: 0..9;

    act: 1..4;

    BEGIN : boolean;
    gOAL : boolean;

ASSIGN

    init(BEGIN) := FALSE;
    next(BEGIN) := 
        case
            (((x_axis = 0) & (y_axis = 0)) | ((x_axis = 1) & (y_axis = 0)) | ((x_axis = 2) & (y_axis = 0))) : TRUE;
            TRUE: BEGIN;
        esac;

    init(gOAL) := FALSE;
    next(gOAL) := 
        case
            (((x_axis = 6) & (y_axis = 9)) | ((x_axis = 7) & (y_axis = 9)) | ((x_axis = 8) & (y_axis = 9))) : TRUE;
            TRUE: gOAL;
        esac;


    -- action: 1:up, 2:down, 3:left, 4:right
    init(act):= 1;
    next(act):=
        case
            -- init
            ((x_axis = 0) & (y_axis = 0)) : {1,4};

            -- obstacles
            ((x_axis = 0) & ((y_axis = 5) | (y_axis = 6) | (y_axis = 7) | (y_axis = 8) | (y_axis = 9))) : act;
            ((x_axis = 1) & ((y_axis = 6) | (y_axis = 7) | (y_axis = 8) | (y_axis = 9))) : act;
            ((x_axis = 2) & ((y_axis = 7) | (y_axis = 8) | (y_axis = 9))) : act;
            ((x_axis = 3) & ((y_axis = 8) | (y_axis = 9))) : act;
            ((x_axis = 4) & (y_axis = 9)) : act;

            ((x_axis = 9) & ((y_axis = 0) | (y_axis = 1) | (y_axis = 2) | (y_axis = 3) | (y_axis = 4))) : act;
            ((x_axis = 8) & ((y_axis = 0) | (y_axis = 1) | (y_axis = 2) | (y_axis = 3))) : act;
            ((x_axis = 7) & ((y_axis = 0) | (y_axis = 1) | (y_axis = 2))) : act;
            ((x_axis = 6) & ((y_axis = 0) | (y_axis = 1))) : act;
            ((x_axis = 5) & (y_axis = 0)) : act;

            -- grids near obstacles
            ((x_axis = 0) & (y_axis = 3)) : {4};
            ((x_axis = 1) & (y_axis = 4)) : {2,4};
            ((x_axis = 2) & (y_axis = 5)) : {2,4};
            ((x_axis = 3) & (y_axis = 6)) : {2,4};
            ((x_axis = 4) & (y_axis = 7)) : {2,4};
            ((x_axis = 5) & (y_axis = 8)) : {4};

            ((x_axis = 3) & (y_axis = 0)) : {1};
            ((x_axis = 4) & (y_axis = 1)) : {1,3};
            ((x_axis = 5) & (y_axis = 2)) : {1,3};
            ((x_axis = 6) & (y_axis = 3)) : {1,3};
            ((x_axis = 7) & (y_axis = 4)) : {1,3};
            ((x_axis = 8) & (y_axis = 5)) : {1};

            --- the boundary of the whole environment
            (x_axis = 0) : {1,4};
            (x_axis = 9) : {2,3};
            (y_axis = 0) : {1,4};
            (y_axis = 9) : {2,3};

            -- else, move to all four directions
            TRUE : {1,2,3,4};
        esac;

    init(x_axis) := {0,1,2};
    next(x_axis) :=
        case
            ((act = 1) | (act = 2)) : x_axis;
            ((x_axis = 0) & (y_axis = 0) & (act = 4)) : {1};
            ((x_axis = 0) & !(y_axis = 0) & (act = 3)) : {1};
            ((x_axis = 0) & !(y_axis = 0) & (act = 4)) : {1};
            ((x_axis = 1) & (act = 3)) : {0};
            ((x_axis = 1) & (act = 4)) : {2};
            ((x_axis = 2) & (act = 3)) : {1};
            ((x_axis = 2) & (act = 4)) : {3};
            ((x_axis = 3) & (act = 3)) : {2};
            ((x_axis = 3) & (act = 4)) : {4};
            ((x_axis = 4) & (act = 3)) : {3};
            ((x_axis = 4) & (act = 4)) : {5};
            ((x_axis = 5) & (act = 3)) : {4};
            ((x_axis = 5) & (act = 4)) : {6};
            ((x_axis = 6) & (act = 3)) : {5};
            ((x_axis = 6) & (act = 4)) : {7};
            ((x_axis = 7) & (act = 3)) : {6};
            ((x_axis = 7) & (act = 4)) : {8};
            ((x_axis = 8) & (act = 3)) : {7};
            ((x_axis = 8) & (act = 4)) : {9};
            ((x_axis = 9) & (act = 3)) : {8};
            TRUE : x_axis;
        esac;


    init(y_axis) := 0;
    next(y_axis) :=
        case
            ((act = 3) | (act = 4)) : y_axis;
            ((y_axis = 0) & (x_axis = 0) & (act = 1)) : {1};

            ((y_axis = 0) & !(x_axis = 0) & (act = 1)) : {1};
            ((y_axis = 0) & !(x_axis = 0) & (act = 2)) : {1};
            ((y_axis = 1) & (act = 2)) : {0};
            ((y_axis = 1) & (act = 1)) : {2};
            ((y_axis = 2) & (act = 2)) : {1};
            ((y_axis = 2) & (act = 1)) : {3};
            ((y_axis = 3) & (act = 2)) : {2};
            ((y_axis = 3) & (act = 1)) : {4};
            ((y_axis = 4) & (act = 2)) : {3};
            ((y_axis = 4) & (act = 1)) : {5};
            ((y_axis = 5) & (act = 2)) : {4};
            ((y_axis = 5) & (act = 1)) : {6};
            ((y_axis = 6) & (act = 2)) : {5};
            ((y_axis = 6) & (act = 1)) : {7};
            ((y_axis = 7) & (act = 2)) : {6};
            ((y_axis = 7) & (act = 1)) : {8};
            ((y_axis = 8) & (act = 2)) : {7};
            ((y_axis = 8) & (act = 1)) : {9};
            ((y_axis = 9) & (act = 2)) : {8};
            TRUE : y_axis;
        esac;

The HyperLTL formula(s)

Path robustness is encoded by forcing any trace that mimics the chosen strategy to reach the goal in lockstep with the witness trace. Once both executions are at the goal, the requirement is satisfied; until then they must agree on the control decisions.

\[\varphi_{\text{rb}} = \exists \pi_A . \forall \pi_B . \big( (strategy_{\pi_B} \leftrightarrow strategy_{\pi_A}) \ \mathcal{U} \ (goal_{\pi_A} \land goal_{\pi_B}) \big)\]

Path Robustness

Exists A . Forall B .
F((act[A]=1) = (act[B]=1))

References

• [NWP19] S. Nalluri, Y. Wang, and M. Pajic. Hyperproperties for robotics: Planning via HyperLTL. In International Conference on Robotics and Automation (ICRA), pages 8011–8017, 2019.