Synthesis of formal control strategies for traffic systems

Bardakçı, Kemal Çağrı
The problems caused by traffic congestion affect human life adversely. Wasted amount of time, fuel and money as well as adverse effects to environment are examples of these problems which reduce life quality. Studies on traffic management underline importance of traffic network control mechanisms. Different configurations of roads and signalized intersections complicate interactions among vehicles and pedestrians. Hence, traffic control systems, which need to satisfy complex specifications, should be constructed to serve complex traffic network features. In this dissertation, we study the problem of synthesizing a signal control strategy for a traffic system from Linear Temporal Logic (LTL) specifications. We focus on scalability issue in formal control of large traffic systems and propose to tackle it by decomposing the main problem into smaller problems. The developed decomposition algorithm partitions main traffic system into subsystems and derives a specification for each subsystem from main specification. In addition, we derive additional constraints on the signals lying on boundaries of subsystems to ensure fairv ness. We employ abstraction based techniques to find control strategies for subsystems by considering dynamics of adjacent subsystems. We show that the controllers found for each system guarantee that overall traffic system satisfies given specification. Moreover, we use bounded LTL, and we analyze effects of bounds on resulting set of satisfying initial states. Furthermore, this dissertation incorporates various optimization criteria into control synthesis. In particular, we developed novel methods to synthesize strategies minimizing the total number of switches and minimizing the maximum vehicle denisty in any link.