Autonomous vehicle operation using linear temporal logic

1. A method comprising:

storing, using one or more processors of a vehicle located at a first spatiotemporal location, a linear temporal logic expression defining an operating constraint for operating the vehicle, wherein the linear temporal logic expression comprises one or more linear temporal logic propositions, wherein a first linear temporal logic proposition of the one or more linear temporal logic propositions represents whether the vehicle is located within an intersection, and wherein a value of the linear temporal logic expression corresponds to whether the vehicle is changing lanes while operating within the intersection;

receiving, using the one or more processors, a second spatiotemporal location for the vehicle;

identifying, using the one or more processors, a motion segment for operating the vehicle from the first spatiotemporal location to the second spatiotemporal location;

determining, using the one or more processors, a value of the linear temporal logic expression based on the motion segment;

generating, using the one or more processors, an operational metric for operating the vehicle in accordance with the motion segment based on the determined value of the linear temporal logic expression; and

causing, using a control module of the vehicle, the vehicle to operate in accordance with the motion segment.

2. The method of claim 1 , wherein a second linear temporal logic proposition of the one or more linear temporal logic propositions represents a lane in which the vehicle is operating.

3. The method of claim 1 , wherein a value of the linear temporal logic expression corresponds to whether the vehicle is operating in a direction specified by the operating constraint.

4. The method of claim 1 , further comprising determining whether causing the vehicle to operate in accordance with the motion segment violates the operating constraint based on the linear temporal logic expression.

5. The method of claim 4 , wherein the determining of whether causing the vehicle to operate in accordance with the motion segment violates the operating constraint is performed responsive to the value of the linear temporal logic expression being false.

6. The method of claim 1 , wherein causing the vehicle to operate in accordance with the motion segment is performed responsive to the operational metric being less than a threshold value.

7. The method of claim 1 , wherein the generating of the operational metric comprises determining a rank of the operating constraint.

8. The method of claim 1 , wherein the operating constraint on operating the vehicle is one of a ranked plurality of operating constraints.

9. The method of claim 1 , further comprising generating a Kripke structure representing the motion segment.

10. The method of claim 9 , wherein a first vertex of the Kripke structure corresponds to the first spatiotemporal location.

11. The method of claim 10 , wherein a second vertex of the Kripke structure corresponds to the second spatiotemporal location.

12. The method of claim 11 , wherein an edge of the Kripke structure connecting the first vertex and the second vertex corresponds to the motion segment for operating the vehicle from the first spatiotemporal location to the second spatiotemporal location.

13. The method of claim 11 , wherein a first value of the linear temporal logic expression evaluated at the first vertex is distinct from a second value of the linear temporal logic expression evaluated at the second vertex.

14. A vehicle comprising:

one or more computer processors; and

one or more non-transitory storage media storing instructions which, when executed by the one or more computer processors, cause the one or more computer processors to:

store a linear temporal logic expression defining an operating constraint for operating the vehicle, wherein the vehicle is located at a first spatiotemporal location wherein the linear temporal logic expression comprises one or more linear temporal logic propositions, wherein a first linear temporal logic proposition of the one or more linear temporal logic propositions represents whether the vehicle is located within an intersection, and wherein a value of the linear temporal logic expression corresponds to whether the vehicle is changing lanes while operating within the intersection;

receive a second spatiotemporal location for the vehicle;

identify a motion segment for operating the vehicle from the first spatiotemporal location to the second spatiotemporal location;

determine a value of the linear temporal logic expression based on the motion segment;

generate an operational metric for operating the vehicle in accordance with the motion segment based on the determined value of the linear temporal logic expression,

causing, using a control module of the vehicle, the vehicle to operate in accordance with the motion segment.

15. The vehicle of claim 14 , wherein the linear temporal logic expression comprises one or more linear temporal logic propositions.

16. One or more non-transitory storage media storing instructions which, when executed by one or more computing devices, cause the one or more computing devices to:

store a linear temporal logic expression defining an operating constraint for operating the vehicle, wherein the vehicle is located at a first spatiotemporal location, wherein the linear temporal logic expression comprises one or more linear temporal logic propositions, wherein a first linear temporal logic proposition of the one or more linear temporal logic propositions represents whether the vehicle is located within an intersection, and wherein a value of the linear temporal logic expression corresponds to whether the vehicle is changing lanes while operating within the intersection;

receive a second spatiotemporal location for the vehicle;

identify a motion segment for operating the vehicle from the first spatiotemporal location to the second spatiotemporal location;

determine a value of the linear temporal logic expression based on the motion segment;

generate an operational metric for operating the vehicle in accordance with the motion segment based on the determined value of the linear temporal logic expression,

causing, using a control module of the vehicle, the vehicle to operate in accordance with the motion segment.