In this project, the complex control objectives for traffic systems are specified in Linear Temporal Logic (LTL) and methods to produce feedback control strategies from these LTL objectives are developed. The control of traffic systems from LTL specifications was studied previously [1], where abstraction based formal control methods were developed for traffic systems.
This project builds on [1] by attacking the main problem in formal synthesis: scalability. In particular, we develop synthesis methods based on network decomposition. The developed method is divides the traffic system into smaller subsystems and derives specifications for these systems. Furthermore, additional constraints on the signals lying on the boundaries of subsystems are introduced to ensure fairness. It is proved that “if each subsystem satisfies its own specification, then the overall traffic system also satisfies the given specification”. Hence the correctness of the synthesized strategy is guaranteed. The correctness result is reached by considering all possible behaviors of the adjacent systems.
A traffic network composed of 9 links and 4 signalized intersections. The flow directions on the links are shown with arrows. The developed method partitions the network into 2 subsystems marked on the figure, and drives a specification for each of them.
tool is available for download
[1] S.Coogan,E.A.Gol,M.Arcak,andC.Belta,“Trafficnetworkcontrol from temporal logic specifications,” IEEE Transactions on Control of Network Systems, vol. 3, no. 2, pp. 162–172, 2016.
Related publications:
Kemal Cagri Bardakci, Ebru Aydin Gol, Formal Control of Traffic Systems Via Network Decomposition, American Control Conference (ACC) 2018.
Kemal Cagri Bardakci, Ebru Aydin Gol, Synthesis of formal control strategies for traffic networks via partitioning, 25th Signal Processing and Communications Applications Conference (SIU) 2017.
This project was funded by Tubitak under 2232 program, grant agreement 116C061 (4/2016-1/2018).