Path planning for robots

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

Case #5.1Case #5.2Case #5.3Case #5.4

The Model(s)

Robotic Robustness 100

--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;

ASSIGN
    -- 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])))