Example 4

Implementation of property "Liveness"

The last example implements the LTL property "Liveness". This property is used to impose that, starting from the current time step, the fact that some properties are satisfied always implies that other will be satisfied in future. In the particular case of the waiter robot task, this property can be used to verify that the execution of the plan is correct. Here, the property to be verified is that each time the robot grabs a coke, a customer will be satisfied in future.

Figures show the DFA and the linear trace associated to the LTL property, and the plan generated by the automated planner. It is easy to verify that the DFA reaches the goal state immediately, but then changes state when the robot grabs the coke, going back to the goal state only when the coke is finally delivered to the customer.

This property was also tested on an extended version of the task, in which there are several drinks and also several customers. In that case also, each time the robot grabs a coke, the DFA drives away from the goal state, going back to it only when the coke is delivered. This last experiment shows how our conversion of LTLf formula to PDDL can easily be scaled and adapted to complex tasks.

Domain

(define(domain robotdomain)

    (:requirements :equality :adl)

    (:predicates

        (happy ?client)

        (robot ?robot)

        (free_arm ?robot)

        (room  ?room)

        (client ?client)

        (coke ?coke)

        (dfa ?dfa)

        (instate ?state)

        (in ?object ?room)

        (update ?dfa)

        (edge ?s-state ?e-state)

        (near ?from-room ?to-room)

        (state ?state)

        (open ?client)

    (: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)

                (state ?e-state)

                (instate state_1)

                (= ?e-state state_2)

                (edge state_1 ?e-state)

                (free_arm ?robot)

                (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)

                (state ?e-state)

                (instate state_2)

                (edge state_2 ?e-state)

                (= ?e-state state_2)

                (free_arm ?robot)

                (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 ?client)

        :precondition

            (and

                (robot ?robot)

                (state ?s-state)

                (state ?e-state)

                (= ?s-state state_1)

                (= ?e-state state_3)

                (instate ?s-state)

                (edge ?s-state ?e-state)

                (not(free_arm ?robot))

                (not(happy ?client))

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate ?s-state))

                (update ?dfa)

    (:action move33

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

        :precondition

            (and

                (robot ?robot)

                (not(in ?robot kitchen)) ; 00

                (instate state_3)

                (edge state_3 ?e-state)

                (= ?e-state state_3)

                (not(happy ?client))

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate state_3))

                (update ?dfa)

    (:action move32

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

        :precondition

            (and

                (robot ?robot)

                (state ?s-state)

                (state ?e-state)

                (= ?s-state state_3)

                (= ?e-state state_2)

                (instate ?s-state)

                (edge ?s-state ?e-state)

                (open ?client)

                (dfa ?dfa)

                (not(update ?dfa))

                (happy ?client)

        :effect

            (and

                (instate ?e-state)

                (not(instate ?s-state))

                (update ?dfa)

    (:action move23

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

        :precondition

            (and

                (robot ?robot)

                (state ?s-state)

                (state ?e-state)

                (client ?client)

                (edge ?s-state ?e-state)

                (= ?s-state state_2)

                (= ?e-state state_3)

                (instate ?s-state)

                (not(free_arm ?robot))

                (not(happy ?client))

                (dfa ?dfa)

                (not(update ?dfa))

        :effect

            (and

                (instate ?e-state)

                (not(instate ?s-state))

                (update ?dfa)

Problem

(define (problem robotproblem)

    (:domain robotdomain)

    (:objects

        livingroom kitchen bedroom corridor hall

        robot_1

        state_1 state_2 state_3 dfa_1

        coke_1 client_1 client_2 coke_2)

    (:init

        (robot robot_1) (client client_1)

        (room livingroom) (room kitchen)

        (room bedroom) (room corridor) (room hall)

        (coke coke_1)(coke coke_2)

        (open client_1) (open client_2)

        (free_arm robot_1)

        (in client_1 livingroom) (in client_2 livingroom)

        (in robot_1 livingroom) (in coke_1 kitchen) (in coke_2 kitchen)

        (near livingroom corridor) (near corridor livingroom)

        (near livingroom bedroom) (near bedroom livingroom)

        (near bedroom kitchen) (near kitchen bedroom)

        (near corridor hall)   (near hall corridor)

        (near hall kitchen)   (near kitchen hall)

        (instate state_1)

        (dfa dfa_1) (update dfa_1)

        (state state_1) (state state_2) (state state_3)

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

        (edge state_3 state_3)  (edge state_3 state_2)

        (edge state_2 state_3)

    (:goal

        (and

            (happy client_1)

            (instate state_2)

            (update dfa_1)

Google Sites

Report abuse