research-article

Formal synthesis of distributed optimal traffic control policies

Authors:

Sadra Sadraddini,

Calin BeltaAuthors Info & Claims

ICCPS '17: Proceedings of the 8th International Conference on Cyber-Physical Systems

Pages 15 - 24

https://doi.org/10.1145/3055004.3055011

Published: 18 April 2017 Publication History

Abstract

We propose a formal methods approach to control traffic signals optimally from specifications described by metric temporal logic (MTL). Since real-time optimization is computationally infeasible beyond small-scale networks, we use a divide and conquer approach. We decompose the network into smaller subnetworks and synthesize assume-guarantee contracts for their interconnections. We show how to exploit mathematical properties of traffic dynamics to find time varying contracts by solving a constraint satisfaction problem. A model predictive control (MPC) approach is used to find local controls for each subnetwork to minimize induced delays, while assume-guarantee contracts and appropriately designed terminal constraints ensure the satisfaction of the specification all over the network. We present a case study on an urban traffic network.

References

[1]

http://sites.bu.edu/hyness/format-distributed. (03/02/2017).

[2]

Rajeev Alur, Salar Moarref, and Ufuk Topcu. 2016. Compositional synthesis with parametric reactive controllers. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. ACM, 215--224.

Digital Library

[3]

Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. 2008. Principles of model checking. MIT press.

[4]

Giacomo Como, Enrico Lovisari, and Ketan Savla. 2016. Convexity and Robustness of Dynamic Network Traffic Assignment for Control of Freeway Networks. IFAC-PapersOnLine 49, 3 (2016), 335--340.

[5]

S Coogan and M Arcak. 2015. Efficient finite abstraction of mixed monotone systems. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, 58--67, 2015. ACM, 58--67.

Digital Library

[6]

Samuel Coogan, Murat Arcak, and Alexander A Kurzhanskiy. 2016. Mixed monotonicity of partial first-in-first-out traffic flow models. In Decision and Control (CDC), 2016 IEEE 55th Conference on. IEEE, 7611--7616.

[7]

S. Coogan, E. A. Gol, M. Arcak, and C. Belta. 2016. Traffic Network Control From Temporal Logic Specifications. IEEE Transactions on Control of Network Systems 3, 2 (June 2016), 162--172.

[8]

Jorge Cortés. 2006. Finite-time convergent gradient flows with applications to network consensus. Automatica 42, 11 (2006), 1993--2000.

Digital Library

[9]

Brian A Davey and Hilary A Priestley. 2002. Introduction to lattices and order. Cambridge university press.

[10]

Adel Dokhanchi, Bardh Hoxha, and Georgios Fainekos. 2014. On-Line Monitoring for Temporal Logic Robustness. In International Conference on Runtime Verification. Springer, 231--246.

[11]

Nathan H Gartner. 1983. OPAC: A Demand-Responsive Strategy for Traffic Signal Control. Transportation Research Record 906 (1983), 75--81.

[12]

Jean Gregoire, Xiangjun Qian, Emilio Frazzoli, Arnaud De La Fortelle, and Tichakorn Wongpiromsarn. 2015. Capacity-aware backpressure traffic signal control. IEEE Transactions on Control of Network Systems 2, 2 (2015), 164--173.

[13]

Wpmh Heemels, B De Schutter, and Alberto Bemporad. 2001. Equivalence of hybrid dynamical models. Automatica 37, 7 (2001), 1085--1091.

Digital Library

[14]

Andreas Hegyi, Bart De Schutter, and Hans Hellendoorn. 2005. Model predictive control for optimal coordination of ramp metering and variable speed limits. Transportation Research Part C: Emerging Technologies 13, 3 (2005), 185--209.

[15]

Thomas A Henzinger, Shaz Qadeer, and Sriram K Rajamani. 1998. You assume, we guarantee: Methodology and case studies. In International Conference on Computer Aided Verification. Springer, 440--451.

[16]

PB Hunt, DI Robertson, RD Bretherton, and RI Winton. 1981. SCOOT-a traffic responsive method of coordinating signals. Technical Report.

[17]

Eric C Kerrigan. 2000. Robust Constraint Satisfaction: Invariant Sets and Predictive Control. Ph.D. Dissertation. University of Cambridge.

[18]

Eric S Kim, Murat Arcak, and Sanjit A Seshia. 2015. Compositional controller synthesis for vehicular traffic networks. In Decision and Control (CDC), 2015 IEEE 54th Annual Conference on. 6165--6171.

[19]

Eric S Kim, Murat Arcak, and Sanjit A Seshia. 2016. Directed Specifications and Assumption Mining for Monotone Dynamical Systems. In Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control. ACM, 21--30.

Digital Library

[20]

Ron Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-Time Systems 2, 4 (1990), 255--299.

Digital Library

[21]

Vito Mauro and C Di Taranto. 1990. Utopia. Control, computers, communications in transportation (1990).

[22]

Pitu Mirchandani and Larry Head. 2001. A real-time traffic signal control system: Architecture, algorithms, and analysis. Transportation Research Part C: Emerging Technologies 9, 6 (2001), 415--432.

[23]

P. Nilsson and N. Ozay. 2016. Synthesis of separable controlled invariant sets for modular local control design. In 2016 American Control Conference (ACC). 5656--5663.

[24]

Markos Papageorgiou, C Diakaki, V Dinopoulou, A Kotsialos, and Yibing Wang. 2003. Review of road traffic control strategies. Proc. IEEE 91, 12 (2003), 2043--2067.

[25]

Vasumathi Raman, Alexandre Donzé, Mehdi Maasoumy, Richard M Murray, Alberto Sangiovanni-Vincentelli, and Sanjit A Seshia. 2014. Model predictive control with signal temporal logic specifications. In 53rd IEEE Conference on Decision and Control. IEEE, 81--87.

[26]

Matthias Rungger and Majid Zamani. 2015. Compositional construction of approximate abstractions. In Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM, 68--77.

Digital Library

[27]

S. Sadraddini and C. Belta. 2015. Robust temporal logic model predictive control. In 2015 53rd Annual Allerton Conference on Communication, Control, and Computing (Allerton). 772--779.

[28]

S. Sadraddini and C. Belta. 2016. Safety control of monotone systems with bounded uncertainties. In 2016 IEEE 55th Conference on Decision and Control (CDC). 4874--4879.

[29]

Sadra Sadraddini and Calin Belta. 2017. Formal Synthesis of Control Strategies for Positive Monotone Systems. (2017). arXiv:arXiv:1702.08501

[30]

Jianbo Shi and Jitendra Malik. 2000. Normalized cuts and image segmentation. IEEE Transactions on pattern analysis and machine intelligence 22, 8 (2000), 888--905.

Digital Library

[31]

Paulo Tabuada and George J. Pappas. 2006. Linear time logic control of discrete-time linear systems. IEEE Trans. Automat. Control 51, 12 (2006), 1862--1877.

[32]

Boyan Yordanov, Jana Tumova, Ivana Cerna, Jiří Barnat, and Calin Belta. 2012. Temporal Logic Control of Discrete-Time Piecewise Affine Systems. IEEE Trans. Automat. Control 57, 6 (2012), 1491--1504.

Cited By

Ghasemi KSadraddini SBelta C(2024)Compositional synthesis for linear systems via convex optimization of assume-guarantee contractsAutomatica10.1016/j.automatica.2024.111816169(111816)Online publication date: Nov-2024
https://doi.org/10.1016/j.automatica.2024.111816
Patil SHashimoto KKishida M(2022)Traffic Flow Control at Signalized Intersections using Signal Spatio-Temporal Logic2022 IEEE 61st Conference on Decision and Control (CDC)10.1109/CDC51059.2022.9993289(1051-1058)Online publication date: 6-Dec-2022
https://doi.org/10.1109/CDC51059.2022.9993289
Al Khatib MStreif S(2021)Synthesis of interconnected control systems under reachability specifications2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683604(1295-1300)Online publication date: 14-Dec-2021
https://doi.org/10.1109/CDC45484.2021.9683604
Show More Cited By

Index Terms

Formal synthesis of distributed optimal traffic control policies

Recommendations

Automatic correct scheduling of control flow intensive behavioral descriptions in formal synthesis
DAC '04: Proceedings of the 41st annual Design Automation Conference

Formal synthesis ensures the correctness of hardware synthesis by automatically deriving the circuit implementation by behavior preserving transformations within a theorem prover. In this paper, we present a new approach to formal synthesis that is able ...
Automated Correctness Condition Generation for Formal Verification ofSynthesized RTL Designs
Special issue on formal methods for computer-added design

High-level synthesis tools generate register-transfer level designs from algorithmic behavioral specifications. The high-level synthesis process typically consists of dependency graph scheduling, functional unit allocation, register allocation, ...
An improved method for traffic control relying on close-loop control theory
CAR'10: Proceedings of the 2nd international Asia conference on Informatics in control, automation and robotics - Volume 3

Urban traffic adaptive control has been considered the most advanced traffic control in the traffic engineering, however, it belongs to the low-level (open-loop control)in the control engineering theory. In recent years, the promotion and application of ...

Comments

Information & Contributors

Information

Published In

cover image ACM Other conferences

ICCPS '17: Proceedings of the 8th International Conference on Cyber-Physical Systems

April 2017

294 pages

ISBN:9781450349659

DOI:10.1145/3055004

General Chairs:
Sonia Martinez
University of California, San Diego
,
Eduardo Tovar
CISTER/INESC TEC, ISEP, Portugal
,
Program Chairs:
Chris Gill
Washington University in St. Louis
,
Bruno Sinopoli
Carnegie Mellon University

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 April 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICCPS '17

ICCPS '17: ACM/IEEE 8th International Conference on Cyber-Physical Systems

April 18 - 20, 2017

Pennsylvania, Pittsburgh

Acceptance Rates

Overall Acceptance Rate 25 of 91 submissions, 27%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
182
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Ghasemi KSadraddini SBelta C(2024)Compositional synthesis for linear systems via convex optimization of assume-guarantee contractsAutomatica10.1016/j.automatica.2024.111816169(111816)Online publication date: Nov-2024
https://doi.org/10.1016/j.automatica.2024.111816
Patil SHashimoto KKishida M(2022)Traffic Flow Control at Signalized Intersections using Signal Spatio-Temporal Logic2022 IEEE 61st Conference on Decision and Control (CDC)10.1109/CDC51059.2022.9993289(1051-1058)Online publication date: 6-Dec-2022
https://doi.org/10.1109/CDC51059.2022.9993289
Al Khatib MStreif S(2021)Synthesis of interconnected control systems under reachability specifications2021 60th IEEE Conference on Decision and Control (CDC)10.1109/CDC45484.2021.9683604(1295-1300)Online publication date: 14-Dec-2021
https://doi.org/10.1109/CDC45484.2021.9683604
Al Khatib MZamani M(2020)Controller synthesis for interconnected systems using parametric assume-guarantee contracts2020 American Control Conference (ACC)10.23919/ACC45564.2020.9147757(5419-5424)Online publication date: Jul-2020
https://doi.org/10.23919/ACC45564.2020.9147757
Ghasemi KSadraddini SBelta CAmes ASeshia SDeshmukh J(2020)Compositional synthesis via a convex parameterization of assume-guarantee contractsProceedings of the 23rd International Conference on Hybrid Systems: Computation and Control10.1145/3365365.3382212(1-10)Online publication date: 22-Apr-2020
https://dl.acm.org/doi/10.1145/3365365.3382212
Belta CSadraddini S(2019)Formal Methods for Control Synthesis: An Optimization PerspectiveAnnual Review of Control, Robotics, and Autonomous Systems10.1146/annurev-control-053018-0237172:1(115-140)Online publication date: 3-May-2019
https://doi.org/10.1146/annurev-control-053018-023717
Liebenwein LSchwarting WVasile CDeCastro JAlonso-Mora JKaraman SRus D(2019)Compositional and Contract-Based Verification for Autonomous Driving on Road NetworksRobotics Research10.1007/978-3-030-28619-4_18(163-181)Online publication date: 28-Nov-2019
https://doi.org/10.1007/978-3-030-28619-4_18
Kim EArcak MSeshia SKim BShiraishi S(2018)Automatic Generation of Communication Requirements for Enforcing Multi-Agent SafetyElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.269.2269(3-16)Online publication date: 10-Apr-2018
https://doi.org/10.4204/EPTCS.269.2
Kim ESadraddini SBelta CArcak MSeshia S(2017)Dynamic contracts for distributed temporal logic control of traffic networks2017 IEEE 56th Annual Conference on Decision and Control (CDC)10.1109/CDC.2017.8264194(3640-3645)Online publication date: Dec-2017
https://doi.org/10.1109/CDC.2017.8264194

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten