Applies when the occurrence of a stimulus triggers a counteraction some time later.
The following formula encodes the mission in LTL for one location. Assume that location l1 must be visited exactly two times:
GLOBALLY (c IMPLIES (NEXT FINALLY (r in l1)))
where “r in l1” is an expression that indicates that a robot r is in a specific area or at a given point.
If a relational notion of space is used, propositions have the form “r in l” where in indicates that the robot r is inside location l and l identifies the desired location. If an absolute notion of space is used, propositions have the form “r at (x,y,z)”, where at indicates that the robot r is in a specific point and (x,y,z) indicates a precise position in space.
Examples and Known Uses
Given a condition c, and the areas l1, l2, l3, and l4 an instantaneous reaction specifies that when c occurs the robot must start moving toward area l1 and l1 is finally reached. If the a robot visits the areas l1, l3, l2, l1, and l4, and c occurs when the robot is in location l2 the mission is satisfied. Vice versa, the mission is not satisfied if a robot visits the areas l1, l3, l2, l1, and l4, and c occurs when the robot is in location l1.
The LTL formula used to encode Delayed Reaction Pattern corresponds to the LTL formula used to encode the Response Pattern by Dwyer modified with the delay represented by the operator NEXT.