??????λ??????????????????????????

针对交通网络中交叉口车流具有连续时间特性，动态信号灯的切换具有离散事件特性的情况，以四相位单交叉口为对象，考虑车辆到达的随机性，以微分包含的形式描述车辆达到率，建立了一个四相位交叉口的矩形混杂自动机模型。该模型中以车辆排队长度为连续状态变量描述连续车流动态，以信号灯状态为离散状态变量描述离散信号灯动态。在该模型基础上,分析了交叉口各个方向的输入、输出车流动态，采用矩形混杂自动机可达性分析方法详细分析了车辆排队长度的可达集，使用CheckMate 3.6 工具箱进行仿真。仿真结果表明矩形混杂自动机模型和可达性分析方法的有效性，不仅能够刻画交叉口车流的动态混杂特性，而且能够验证信号灯配时方案对车流疏导是否有效，为信号灯配时设计提供一种检验方法。

Modeling and Reachability Analysis for Single Intersection Based on Rectangular Hybrid Automata

Vehicle flow show continuous behavior and traffic light exhibit discrete event behavior, thus a rectangular hybrid automata model of a four-phase intersection is proposed in this paper. The queue lengths are considered as continuous variables to represent the vehicle flow behavior of the intersection, and the discrete event part are used to reflect the discrete characteristics traffic light. Based on the rectangular hybrid automata model, all directional vehicle flows are analyzed. A method for reachability analysis of rectangular hybrid automata is applied to examine the maximum and minimum of each queue length of the single intersection. The simulation based on toolbox CheckMate 3.6 shows that the rectangular hybrid automata model not only perfectly represents the hybrid characters of the dynamic traffic flow of the single intersection, but also verifies the efficiency of the time scheme of the traffic light.