# Safety Verification of Driving Resource Occupancy Rules Based on Functional Language
## 2 Related Work  
The current research on the environment of automatic driving mainly focuses on the decision-making of safe driving and environmental perception.  
Aiming at the decision-making of safe driving, [PERSON] [18] et al. studied the influence of the driver's state on driving, thereby modeling and verifying the driver's state. [PERSON] [19] et al. proposed multi strategy decision making, by assuming that the controlled vehicles and other traffic participants execute a strategy from a set of plausible closed-loop strategies at each time step, so as to find the best strategy that can be executed by controlling vehicles.  
For environment perception, [PERSON] [20] et al. proposed a method to enhance the standard dynamic target tracker. On the one hand, it estimates the occlusion state of other traffic agents, on the other hand, it closely links the occlusion estimation with the new observation data after the tracked target reenters. [PERSON] [14] et al. abstracted the environment and mapped it to Stochastic Hybrid Automata to study the probability of occurrence of events to quantitatively describe uncertain events. [PERSON] [21] et al. also used the environment as a reference, combining language and indicating gestures to guide the car. [PERSON] [22] et al. simulated the variable phase traffic light control system and identified its accident scenarios to avoid accidents completely. [PERSON] [23] et al. summarized the taxi scheduling problem in autonomous driving. [PERSON] [24] et al. shared their research on building a production distributed autonomous driving simulation platform. [PERSON] [25] et al. proposed a safety risk intelligent prediction model for the train control system to predict which risk state will occur under specific operating conditions. [PERSON] [26] et al. consider the delay of driver behavior to verify the automatic driving system in the model test.  
Some researchers focus on motion planning problems for autonomous driving [27; 28; 29]. [PERSON] [30] et al. proposed an advanced prediction scheme for motion planning from three aspects: risk evaluation, criteria minimization, and constraint submission. The detailed conditions of motion planning are described under the framework of highway and restricted environment with small curvature and specific driver rules, and the corresponding motion planning algorithm is proposed. [PERSON] [31] et al. proposed a novel Integrated Local Trajectory Planning and Tracking Control (ILTPTC) framework for autonomous vehicles traveling along a reference path and avoiding obstacles. The framework adopts an efficient state-space sampling-based trajectory planning scheme to smoothly follow the reference path. A model-based predictive path generation algorithm is applied to generate a set of feasible motion paths that take into account both motion speed and driver safety and comfort.  
In addition, there are some studies to improve the safety of automatic driving from the technical aspect. Considering the environmental changes caused by the appearance changes caused by short-term (such as weather, light) and long-term (such as season, vegetation growth, etc.), literature [19] proposed a new location recognition technology, which can effectively retrain and compress. [PERSON] [32] et al. described the method in the field of deep learning image recognition.  
Compared with the above research work, this paper extracts the automatic driving environment model, maps the running cars into processes, maps the roads into corresponding resources, maps the driving of cars on the roads into the occupation of resources and specifies a series of transformation rules to convert the environment model into a process algebra model for verification. It provides a new idea for the research of the automatic driving model. In addition, using algebra to abstract the environment model can effectively improve the formulation of environment model strategy and ensure the safety of automatic driving.