Shortest Paths: Grid-World Planning (NuSMV)

Description of the Case Study

We use HyperQB to synthesise optimal strategies for a mobile robot navigating a grid world [NWP19]. The agent starts in the lower-left corner and must reach the upper-right goal cell while avoiding unnecessary detours. The shortest-path HyperLTL specification asks for a strategy whose execution reaches the goal no later than any competing run. HyperQB searches for such a trace in grids up to \(60 \times 60\) (3,600 cells) and returns SAT, yielding a controller that is globally optimal with respect to the goal-reaching time.

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..10;
    y_axis: 0..10;

    TOKEN: 0..1;

    gOAL: boolean;
    LEFT : boolean;
    RIGHT: boolean;
    UP   : boolean;
    DOWN : boolean;


    

ASSIGN
    init(gOAL) := FALSE;
    next(gOAL) := 
        case 
            ((x_axis=7 & y_axis=5)): TRUE;
            TRUE: gOAL;
        esac;


    init(LEFT) := FALSE;
    next(LEFT) := (!(x_axis=0))
                & !(x_axis=7 & y_axis=6)
                & !(x_axis=8 & y_axis=6)
                & !(x_axis=5 & y_axis=5)
                & !(x_axis=4 & y_axis=4)
                & !(x_axis=6 & y_axis=4)
                & !(x_axis=2 & y_axis=8)
                & !(x_axis=7 & y_axis=4)
                & !(x_axis=5 & y_axis=9)
                & !(x_axis=3 & y_axis=6)
                & !(x_axis=5 & y_axis=6)
                & !(x_axis=2 & y_axis=5)
                & !(x_axis=7 & y_axis=3)
                & !(x_axis=3 & y_axis=9)
                & !(x_axis=9 & y_axis=5)
                & !(x_axis=4 & y_axis=5)
                & !(x_axis=4 & y_axis=1)
                & !(x_axis=6 & y_axis=0)
                & !(x_axis=9 & y_axis=6)
                & !(x_axis=2 & y_axis=6)
                & !(x_axis=4 & y_axis=6)
                & !(x_axis=4 & y_axis=8)
                & !(x_axis=2 & y_axis=9)
                & !(x_axis=3 & y_axis=8)
                & !(x_axis=8 & y_axis=4)
                & !(x_axis=2 & y_axis=3);


    init(RIGHT) := FALSE;
    next(RIGHT) := (!(x_axis=9))
                & !(x_axis=5 & y_axis=4)
                & !(x_axis=7 & y_axis=6)
                & !(x_axis=7 & y_axis=5)
                & !(x_axis=4 & y_axis=0)
                & !(x_axis=4 & y_axis=4)
                & !(x_axis=6 & y_axis=6)
                & !(x_axis=6 & y_axis=4)
                & !(x_axis=2 & y_axis=8)
                & !(x_axis=2 & y_axis=4)
                & !(x_axis=3 & y_axis=6)
                & !(x_axis=1 & y_axis=6)
                & !(x_axis=8 & y_axis=1)
                & !(x_axis=2 & y_axis=1)
                & !(x_axis=5 & y_axis=6)
                & !(x_axis=2 & y_axis=5)
                & !(x_axis=0 & y_axis=3)
                & !(x_axis=5 & y_axis=3)
                & !(x_axis=3 & y_axis=9)
                & !(x_axis=1 & y_axis=8)
                & !(x_axis=0 & y_axis=6)
                & !(x_axis=0 & y_axis=9)
                & !(x_axis=2 & y_axis=6)
                & !(x_axis=1 & y_axis=9)
                & !(x_axis=0 & y_axis=8)
                & !(x_axis=3 & y_axis=5)
                & !(x_axis=0 & y_axis=5);

    
    init(UP):= FALSE;
    next(UP):= (!(y_axis=9))
                & !(x_axis=3 & y_axis=3)
                & !(x_axis=1 & y_axis=4)
                & !(x_axis=3 & y_axis=0)
                & !(x_axis=8 & y_axis=5)
                & !(x_axis=3 & y_axis=4)
                & !(x_axis=7 & y_axis=5)
                & !(x_axis=4 & y_axis=4)
                & !(x_axis=2 & y_axis=7)
                & !(x_axis=1 & y_axis=5)
                & !(x_axis=6 & y_axis=5)
                & !(x_axis=2 & y_axis=8)
                & !(x_axis=6 & y_axis=2)
                & !(x_axis=3 & y_axis=7)
                & !(x_axis=2 & y_axis=5)
                & !(x_axis=7 & y_axis=3)
                & !(x_axis=5 & y_axis=3)
                & !(x_axis=4 & y_axis=5)
                & !(x_axis=1 & y_axis=8)
                & !(x_axis=9 & y_axis=0)
                & !(x_axis=1 & y_axis=7)
                & !(x_axis=6 & y_axis=3)
                & !(x_axis=4 & y_axis=8)
                & !(x_axis=1 & y_axis=2)
                & !(x_axis=3 & y_axis=5)
                & !(x_axis=8 & y_axis=4);

    
    init(DOWN) := FALSE;
    next(DOWN) := (!(y_axis=0))
                & !(x_axis=1 & y_axis=4)
                & !(x_axis=8 & y_axis=6)
                & !(x_axis=5 & y_axis=5)
                & !(x_axis=7 & y_axis=5)
                & !(x_axis=8 & y_axis=7)
                & !(x_axis=2 & y_axis=7)
                & !(x_axis=6 & y_axis=5)
                & !(x_axis=6 & y_axis=4)
                & !(x_axis=4 & y_axis=7)
                & !(x_axis=7 & y_axis=7)
                & !(x_axis=3 & y_axis=6)
                & !(x_axis=3 & y_axis=7)
                & !(x_axis=1 & y_axis=6)
                & !(x_axis=6 & y_axis=7)
                & !(x_axis=3 & y_axis=2)
                & !(x_axis=3 & y_axis=9)
                & !(x_axis=4 & y_axis=6)
                & !(x_axis=1 & y_axis=9)
                & !(x_axis=1 & y_axis=7)
                & !(x_axis=9 & y_axis=2)
                & !(x_axis=2 & y_axis=9)
                & !(x_axis=5 & y_axis=1)
                & !(x_axis=3 & y_axis=5);



    init(TOKEN):= 0;
    next(TOKEN):= {0,1};

    init(x_axis) := {0};
    next(x_axis) :=
        case
            (TOKEN=0) : x_axis;
            (x_axis=0 & RIGHT ) : {1};
            (x_axis=1 & LEFT & RIGHT) : {0,2};
            (x_axis=1 & LEFT & !RIGHT) : {0};
            (x_axis=1 & !LEFT & RIGHT) : {2};
            (x_axis=2 & LEFT & RIGHT) : {1,3};
            (x_axis=2 & LEFT & !RIGHT) : {1};
            (x_axis=2 & !LEFT & RIGHT) : {3};
            (x_axis=3 & LEFT & RIGHT) : {2,4};
            (x_axis=3 & LEFT & !RIGHT) : {2};
            (x_axis=3 & !LEFT & RIGHT) : {4};
            (x_axis=4 & LEFT & RIGHT) : {3,5};
            (x_axis=4 & LEFT & !RIGHT) : {3};
            (x_axis=4 & !LEFT & RIGHT) : {5};
            (x_axis=5 & LEFT & RIGHT) : {4,6};
            (x_axis=5 & LEFT & !RIGHT) : {4};
            (x_axis=5 & !LEFT & RIGHT) : {6};
            (x_axis=6 & LEFT & RIGHT) : {5,7};
            (x_axis=6 & LEFT & !RIGHT) : {5};
            (x_axis=6 & !LEFT & RIGHT) : {7};
            (x_axis=7 & LEFT & RIGHT) : {6,8};
            (x_axis=7 & LEFT & !RIGHT) : {6};
            (x_axis=7 & !LEFT & RIGHT) : {8};
            (x_axis=8 & LEFT & RIGHT) : {7,9};
            (x_axis=8 & LEFT & !RIGHT) : {7};
            (x_axis=8 & !LEFT & RIGHT) : {9};
            (x_axis=9 & LEFT & RIGHT) : {8,10};
            (x_axis=9 & LEFT & !RIGHT) : {8};
            (x_axis=9 & !LEFT & RIGHT) : {10};

            TRUE: x_axis;
        esac;


    init(y_axis) := 0;
    next(y_axis) :=
        case
            (TOKEN=1) : y_axis;
            (y_axis=0 & UP) : {1};

            (y_axis=1 & UP & DOWN) : {2,0};
            (y_axis=1 & UP & !DOWN) : {2};
            (y_axis=1 & !UP & DOWN) : {0};
            (y_axis=2 & UP & DOWN) : {3,1};
            (y_axis=2 & UP & !DOWN) : {3};
            (y_axis=2 & !UP & DOWN) : {1};
            (y_axis=3 & UP & DOWN) : {4,2};
            (y_axis=3 & UP & !DOWN) : {4};
            (y_axis=3 & !UP & DOWN) : {2};
            (y_axis=4 & UP & DOWN) : {5,3};
            (y_axis=4 & UP & !DOWN) : {5};
            (y_axis=4 & !UP & DOWN) : {3};
            (y_axis=5 & UP & DOWN) : {6,4};
            (y_axis=5 & UP & !DOWN) : {6};
            (y_axis=5 & !UP & DOWN) : {4}; 
            (y_axis=6 & UP & DOWN) : {7,5};
            (y_axis=6 & UP & !DOWN) : {7};
            (y_axis=6 & !UP & DOWN) : {5};
            (y_axis=7 & UP & DOWN) : {8,6};
            (y_axis=7 & UP & !DOWN) : {8};
            (y_axis=7 & !UP & DOWN) : {6};
            (y_axis=8 & UP & DOWN) : {9,7};
            (y_axis=8 & UP & !DOWN) : {9};
            (y_axis=8 & !UP & DOWN) : {7};
            (y_axis=9 & UP & DOWN) : {10,8};
            (y_axis=9 & UP & !DOWN) : {10};
            (y_axis=9 & !UP & DOWN) : {8};
            
            TRUE: y_axis;
        esac;

The HyperLTL formula(s)

The shortest-path requirement states that there exists a trace \(\pi_A\) whose goal is reached before any alternative trace \(\pi_B\). Until \(\pi_A\) visits the goal, \(\pi_B\) must remain in non-goal states, ensuring that \(\pi_A\) arrives at the goal in the minimal number of steps.

\[\varphi_{\text{sp}} = \exists \pi_A . \forall \pi_B . \big( \neg\, goal_{\pi_B} \ \mathcal{U} \ goal_{\pi_A} \big)\]

Shortest Path

Exists A . Forall B .
F(gOAL[A]) & G(( (~(gOAL[A]))) -> (~(gOAL[B])))

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.