Path planning for robots (NuSMV)

Description of the Case Study

In this case study we use HyperQB beyond verification, to synthesize strategies for robotic planning [NWP19]. Here, we focus on producing a strategy that satisfies control requirements for a robot to reach a goal in a grid. First, the robot should take the shortest path, expressed as:

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

We also used HyperQB to solve the path robustness problem, meaning that starting from an arbitrary initial state, a robot reaches the goal by following a single strategy, expressed as:

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

HyperQB returns SAT for the grids of sizes up to \(60 \times 60\).

Benchmarks

The Model(s)

--ROBOTIC PLANNING
--(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;

DEFINE
    -- BEGIN := (((x_axis = 0) & (y_axis = 0)) | ((x_axis = 1) & (y_axis = 0)) | ((x_axis = 2) & (y_axis = 0)));
    -- gOAL := (((x_axis = 6) & (y_axis = 9)) | ((x_axis = 7) & (y_axis = 9)) | ((x_axis = 8) & (y_axis = 9)));

Formula

Exists A . Forall B .
F(gOAL[A])
& (G(((act[A]=1) =  (act[B]=1))
&((act[A]=2) = (act[B]=2))
&((act[A]=3) = (act[B]=3))
&((act[A]=4) = (act[B]=4)))
-> (F(gOAL[B])))

References