Formal Control of Traffic Systems via Network Decomposition

We study the problem of synthesizing a signal control strategy for a traffic system from Linear Temporal Logic specifications. In particular, we focus on the scalability issue in the formal control of large traffic systems and propose to tackle it by decomposing the main problem into smaller problems. The developed decomposition algorithm partitions the main traffic system into subsystems and derives a specification for each subsystem from the main specification. In addition, we derive additional constraints on the signals lying on the boundaries of subsystems to ensure fairness. Abstraction based techniques are employed to find control strategies for subsystems. During the computation of a finite abstraction, the dynamics and specifications of adjacent systems are also considered. We show that the controllers found for each system guarantee that the main traffic system satisfies the given specification.