Example 1

Implementation of operator "Next"

The first simple example implements the LTL operator "Next". This type of operator is used to impose that, starting from the current time step, in the next one some properties have to be verified. In the particular case of the waiter robot task, this operator can be used to impose a constraint on the first step of the robot path while reach its goal. Here, the constraint to be satisfied is that the robot is in the bedroom at next state, and thus continuing to accomplish its task by freely choosing the rest of the path.

Figures show the DFA and the linear trace associated to the LTL formula, and the plan generated by the automated planner. It is easy to verify how the robot is obliged to take the way of the bedroom while going to the kitchen, and is instead free to choose the other way while going back to living room. In fact, the DFA reaches the goal state immediately after the first update and stays there for the rest of the plan execution.

Domain

(define(domain robotdomain)

    (:requirements :equality)

    (:predicates

        (happy ?client)

        (robot ?robot)

        (free_arm ?robot)

        (room  ?room)

        (client ?client)

        (coke ?coke)

        (dfa ?dfa)

        (instate ?state)

        (in ?object ?room)

        (update ?dfa)

        (near ?from-room ?to-room)

        (edge ?s-state ?e-state)

        (state ?state)

    (:action go_to

         :parameters (?robot ?from-room ?to-room ?dfa)

         :precondition

             (and

                 (robot ?robot)

                 (room ?from-room)

                 (room ?to-room)

                 (near ?from-room ?to-room)

                 (in ?robot ?from-room)

                 (dfa ?dfa)

                 (update ?dfa)

          :effect

            (and

                (not (in ?robot ?from-room))

                (in ?robot ?to-room)

                (not(update ?dfa))

    (:action grab

        :parameters(?robot ?coke ?room ?dfa)

        :precondition

            (and

                (robot ?robot)

                (coke ?coke)

                (free_arm ?robot)

                (dfa ?dfa)

                (update ?dfa)

                (in ?robot ?room)

                (in ?coke ?room)

        :effect

            (and

                (not (free_arm ?robot))

                (not (update ?dfa))

                (not (in ?coke ?room))

    (:action give_to

        :parameters (?robot ?client ?coke ?where-room ?dfa)

        :precondition

            (and

                (robot ?robot)

                (coke ?coke)

                (in ?robot ?where-room)

                (in ?client ?where-room)

                (not (free_arm ?robot))

                (dfa ?dfa)

                (update ?dfa)

        :effect

            (and

                (free_arm ?robot)

                (happy ?client)

                (not(update ?dfa))

    (:action move12

        :parameters(?robot ?e-state ?dfa)

        :precondition

            (and

                (robot ?robot)

                (in ?robot bedroom) ; X(in robot kitchen)

                (instate state_1)

                (edge state_1 ?e-state)

                (= ?e-state state_2)

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate state_1))

                (update ?dfa)

   (:action move22

        :parameters(?robot ?e-state ?dfa)

        :precondition

            (and

                (robot ?robot)

                (instate state_2)

                (edge state_2 ?e-state)

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate state_2))

                (update ?dfa)

    (:action move13

        :parameters(?robot ?s-state ?e-state ?dfa)

        :precondition

            (and

                (robot ?robot)

                (not(in ?robot bedroom))

                (instate state_1)

                (edge state_1 ?e-state)

                (= ?e-state state_3)

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate state_1))

                (update ?dfa)

    (:action move33

        :parameters(?robot ?e-state ?dfa)

        :precondition

            (and

                (robot ?robot)

                (not(in ?robot kitchen))

                (instate state_3)

                (edge state_3 ?e-state)

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate state_3))

                (update ?dfa)

Problem

(define (problem robotproblem)

    (:domain robotdomain)

    (:objects

        livingroom kitchen bedroom bathroom corridor hall

        robot_1

        client_1 client_2 coke_1 coke_2

        dfa_1

        state_1 state_2 state_3

    (:init

        (robot robot_1) (client client_1)

        (room livingroom) (room kitchen)

        (room hall) (room corridor)

        (room bedroom) (room bathroom)

        (near livingroom corridor) (near corridor livingroom)

        (near livingroom bedroom) (near bedroom livingroom)

        (near corridor hall) (near hall corridor)

        (near hall kitchen) (near kitchen hall)

        (near bathroom kitchen) (near kitchen bathroom)

        (near bathroom bedroom) (near bedroom bathroom)

        (in robot_1 livingroom)  (instate state_1)

        (dfa dfa_1) (update dfa_1)

        (edge state_1 state_2) (edge state_1 state_3) (edge state_2 state_2) (edge state_3 state_3)

        (coke coke_1) (coke coke_2)

        (free_arm robot_1) (in coke_1 kitchen) (in coke_2 kitchen)

        (in client_1 livingroom) (in client_2 livingroom)

    (:goal

        (and

            (happy client_1) (instate state_2)

Google Sites

Report abuse