A bounded multi-dimensional modal logic for autonomous cars based on local traffic and estimation

The decision-making module on an autonomous car is usually a periodic program. In every cycle, the program makes a decision such as acceleration, brake, initiating a lane change process or a turn process based on the current traffic information gathered from car sensors. In urban traffic with mixed type of vehicles, the real-time performance requirement is critical for the decision-making program while acquiring global knowledge of the traffic is less practical. In such an environment, communications between vehicles are unreliable and time-consuming, so it is often difficult to know the exact driving decisions of other cars in the next cycle. In order to guarantee safety, a feasible solution requires the reasonable estimation on the driving decisions of other cars in the near future. In this paper, we propose a BMML (Bounded Multi-dimensional Modal Logic) to specify the traffic situations with spatio-temproral properties taking account of the estimated evolvement on them in the near future. The logic contains a primitive spatial logic with navigation operators and estimation operators as modal operators. The satisfaction of a BMML formula depends on a snapshot of the current traffic condition and an estimation structure capturing the believed information on the driving decisions of other cars. Given a snapshot and an estimation structure, the satisfaction of a BMML formula can be determined with simple and deterministic reasoning, so it is feasible for taking a BMML formula as the guard condition of the decision-making program of an autonomous car. The usage of BMML is illustrated with a series of small examples.