Specification Guided Automated Synthesis of Feedback Controllers
Article No.: 80, Pages 1 - 26
Abstract
The growing use of complex Cyber-Physical Systems (CPSs) in safety-critical applications has led to the demand for the automatic synthesis of robust feedback controllers that satisfy a given set of formal specifications. Controller synthesis from the high-level specification is an NP-Hard problem. We propose a heuristic-based automated technique that synthesizes feedback controllers guided by Signal Temporal Logic (STL) specifications. Our technique involves rigorous analysis of the traces generated by the closed-loop system, matrix decomposition, and an incremental multi-parameter tuning procedure. In case a controller cannot be found to satisfy all the specifications, we propose a technique for modifying the unsatisfiable specifications so that the controller synthesized for the satisfiable subset of specifications now also satisfies the modified specifications. We demonstrate our technique on eleven controllers used as standard closed-loop control system benchmarks, including complex controllers having multiple independent or nested control loops. Our experimental results establish that the proposed algorithm can automatically solve complex feedback controller synthesis problems within a few minutes.
References
[1]
Y. Annpureddy, C. Liu, G. E. Fainekos, and S. Sankaranarayanan. 2011. S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In TACAS. 254–257.
[2]
E. Asarin, A. Donzé, O. Maler, and D. Nickovic. 2011. Parametric identification of temporal properties. In RV. 147–160.
[3]
K. J. Astrom and R. M. Murray. 2008. Feedback Systems: An Introduction for Scientists and Engineers. Princeton University Press, USA.
[4]
D. P. Atherton. 2000. Autotuning of PID controllers: Relay feedback approach. Int. J. Adapt. Control Signal Process. 14, 5 (2000), 559–562.
[5]
E. Bartocci, T. Ferrère, N. Manjunath, and D. Ničković. 2018. Localizing Faults in simulink/stateflow models with STL. In HSCC. ACM, 197–206.
[6]
V. Blondel and J. N. Tsitsiklis. 1997. NP-Hardness of some linear control design problems. SIAM J. Control Optim. 35, 6 (1997), 2118–2127.
[7]
S. Bogomolov, C. Mitrohin, and A. Podelski. 2010. Composing reachability analyses of hybrid systems for safety and stability. In ATVA. 67–81.
[8]
A. K. Bozkurt, Y. Wang, M. M. Zavlanos, and M. Pajic. 2020. Control synthesis from linear temporal logic specifications using model-free reinforcement learning. In ICRA. IEEE, 10349–10355.
[9]
T. F. Chan. 1987. Rank revealing QR factorizations. Linear Algebra Appl. 88–89 (1987), 67–82.
[10]
CTMS. [n.d.]. Aircraft Pitch. http://ctms.engin.umich.edu/CTMS/index.php?example=AircraftPitch§ion=SimulinkModeling.
[11]
CTMS. [n.d.]. DC Motor. http://ctms.engin.umich.edu/CTMS/index.php?example=MotorSpeed§ion=Sim ulinkModeling.
[12]
CTMS. [n.d.]. Inverted Pendulum. http://ctms.engin.umich.edu/CTMS/index.php?example=InvertedPendulum§i on=SimulinkModeling.
[13]
R. Dimitrova, M. Ghasemi, and U. Topcu. 2020. Reactive synthesis with maximum realizability of linear temporal logic specifications. Acta Informatica 57, 1–2 (2020), 107–135.
[14]
A. Donzé. 2010. Breach: A toolbox for verification and parameter synthesis of hybrid systems. In CAV. 167–170.
[15]
A. Donzé, T. Ferrère, and O. Maler. 2013. Efficient robust monitoring for STL. In CAV. 264–279.
[16]
E. A. Lee and S. A. Seshia. 2017. Introduction to Embedded Systems - A Cyber-Physical Systems Approach, Second Edition. MIT Press.
[17]
C. Finucane, G. Jing, and H. Kress-Gazit. 2010. LTLMoP: Experimenting with language, temporal logic and robot control. In IROS. 1988–1993.
[18]
S. Ghosh, D. Sadigh, P. Nuzzo, V. Raman, A. Donzé, A. L. Sangiovanni-Vincentelli, S. S. Sastry, and S. A. Seshia. 2016. Diagnosis and repair for synthesis from signal temporal logic specifications. In HSCC. 31–40.
[19]
G. H. Golub and Charles F. V. Loan. 1996. Matrix Computations (3 ed.). Johns Hopkins.
[20]
Y. P. Hong and C. T. Pan. 1992. Rank-revealing QR factorizations and the singular value decomposition. Math. Comp. 58, 197 (1992), 213–232.
[21]
J. Hwangbo, I. Sa, R. Siegwart, and M. Hutter. 2017. Control of a quadrotor with reinforcement learning. IEEE Robotics and Automation Letters 2, 4 (2017), 2096–2103.
[22]
S. Jha, S. Raj, S. K. Jha, and N. Shankar. 2018. Duality-based nested controller synthesis from STL specifications for stochastic linear systems. In FORMATS. 235–251.
[23]
X. Jin, A. Donzé, J. V. Deshmukh, and S. A. Seshia. 2015. Mining requirements from closed-loop control models. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 34, 11 (2015), 1704–1717.
[24]
G. Juniwal, A. Donzé, J. C. Jensen, and S. A. Seshia. 2014. CPSGrader: Synthesizing temporal logic testers for auto-grading an embedded systems laboratory. In EMSOFT. 24:1–24:10.
[25]
J. Kapinski, X. Jin, J. Deshmukh, A. Donze, T. Yamaguchi, H. Ito, T. Kaga, S. Kobuna, and S. Seshia. 2016. ST-Lib: A library for specifying and classifying model behaviors. In SAE Technical Paper. SAE International.
[26]
I. M. Khairuddin, A. Majeed, A. Lim, J. A. Jizat, and A. A. Jaafar. 2014. Modelling and PID control of a quadrotor aerial robot. In Manufacturing Engineering(Advanced Materials Research, Vol. 903). 327–331.
[27]
R. Koymans. 1990. Specifying real-time properties with metric temporal logic. Real-Time Systems 2, 4 (1990), 255–299.
[28]
Timothy P. Lillicrap, Jonathan J. Hunt, Alexander Pritzel, Nicolas Heess, Tom Erez, Yuval Tassa, David Silver, and Daan Wierstra. 2016. Continuous control with deep reinforcement learning. In ICLR.
[29]
J. Lygeros, C. Tomlin, and S. Sastry. 1997. Multiobjective hybrid controller synthesis. In Hybrid and Real-Time Systems, O. Maler (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 109–123.
[30]
O. Maler and D. Nickovic. 2013. Monitoring properties of analog and mixed-signal circuits. STTT 15, 3 (2013), 247–268.
[31]
MathWorks. [n.d.]. Cascaded Multiloop Feedback Design. https://www.mathworks.com/help/control/ug/cascaded-multi-loopmulti-compen sator-feedback-design.html.
[32]
MathWorks. [n.d.]. Designing a High Angle of Attack Pitch Mode Control. https://www.mathworks.com/help/simulink/slref/designing-a-high-angle-of-a ttack-pitch-mode-control.html.
[33]
MathWorks. [n.d.]. Fixed-Structure Autopilot for a Passenger Jet. https://www.mathworks.com/help/control/ug/fixed-structure-autopilot-for-a -passenger-jet.html.
[34]
MathWorks. [n.d.]. QR decomposition. https://in.mathworks.com/help/matlab/ref/qr.html.
[35]
MathWorks. [n.d.]. Temperature Control in a Heat Exchanger. https://www.mathworks.com/help/control/ug/temperature-control-in-a-heat-e xchanger.html.
[36]
M. Mazo, A. Davitian, and P. Tabuada. 2010. PESSOA: A tool for embedded controller synthesis. In CAV. 566–569.
[37]
L. Meier, D. Honegger, and M. Pollefeys. 2015. PX4: A node-based multithreaded open source robotics framework for deeply embedded platforms. ICRA, 6235–6240.
[38]
P. M. Meshram and R. G. Kanojiya. 2012. Tuning of PID controller using Ziegler-Nichols method for speed control of DC motor. In ICAESM. 117–122.
[39]
S. Mouelhi, A. Girard, and G. Gössler. 2013. CoSyMA: A tool for controller synthesis using multi-scale abstractions. In HSCC. 83–88.
[40]
D. Nickovic and O. Maler. 2007. AMT: A Property-based monitoring tool for analog systems. In FORMATS. 304–319.
[41]
A. Pnueli. 1977. The temporal logic of programs. In SFCS. 46–57.
[42]
Quanser Real-Time Control (QUARC. [n.d.]. CRS Robot Arm. http://quanser-update.azurewebsites.net/quarc/documentation/quarc_using_d evices_robots.html#catalyst.
[43]
V. Raman, A. Donzé, D. Sadigh, R. M. Murray, and S. A. Seshia. 2015. Reactive synthesis from signal temporal logic specifications. In HSCC. 239–248.
[44]
V. Raman, A. Donzé, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, and S. A. Seshia. 2014. Model predictive control with signal temporal logic specifications. In CDC. 81–87.
[45]
P. Roy, P. Tabuada, and R. Majumdar. 2011. Pessoa 2.0: A controller synthesis tool for cyber-physical systems. In HSCC. 315–316.
[46]
W. Selby. [n.d.]. Simulating a 3DRobotics ArduPilot based quadrotor. https://www.wilselby.com/research/arducopter/controller-design/.
[47]
F. Shmarov, N. Paoletti, E. Bartocci, S. Lin, S. A. Smolka, and P. Zuliani. 2017. SMT-based synthesis of safe and robust pid controllers for stochastic hybrid systems. In Hardware and Software: Verification and Testing. 131–146.
[48]
A. Silberschatz, H. Korth, and S. Sudarshan. 2005. Database Systems Concepts (5 ed.). McGraw-Hill, Inc., USA.
[49]
N. K. Singh and I. Saha. 2020. Specification-guided automated debugging of CPS models. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39, 11 (2020), 4142–4153.
[50]
P. Varshney, G. Nagar, and I. Saha. 2019. DeepControl: Energy-efficient control of a quadrotor using a deep neural network. In IROS. 43–50.
[51]
T. Wongpiromsarn, U. Topcu, N. Ozay, Huan Xu, and R. M. Murray. 2011. TuLiP: A software toolbox for receding horizon temporal logic planning. In HSCC. 313–314.
[52]
M. Zhuang and D. P. Atherton. 1993. Automatic tuning of optimum PID controllers. IEE Proceedings D - Control Theory and Applications 140, 3 (1993), 216–224.
Index Terms
- Specification Guided Automated Synthesis of Feedback Controllers
Recommendations
Compositional Synthesis with Parametric Reactive Controllers
HSCC '16: Proceedings of the 19th International Conference on Hybrid Systems: Computation and ControlReactive synthesis with the ambitious goal of automatically synthesizing correct-by-construction controllers from high-level specifications, has recently attracted significant attention in system design and control. In practice, complex systems are ...
Design of PI and PID controllers with transient performance specification
Proportional-integral-derivative (PID) controllers are widely used in industrial control systems because of the reduced number of parameters to be tuned. The most popular design technique is the Ziegler-Nichols method, which relies solely on parameters ...
PuRSUE -from specification of robotic environments to synthesis of controllers
AbstractDeveloping robotic applications is a complex task, which requires skills that are usually only possessed by highly-qualified robotic developers. While formal methods that help developers in the creation and design of robotic applications exist, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2021
1367 pages
Copyright © 2021 Association for Computing Machinery.
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
Journal Family
Publication History
Published: 22 September 2021
Accepted: 01 July 2021
Revised: 01 June 2021
Received: 01 April 2021
Published in TECS Volume 20, Issue 5s
Check for updates
Author Tags
Qualifiers
- Research-article
- Refereed
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 156Total Downloads
- Downloads (Last 12 months)26
- Downloads (Last 6 weeks)5
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign inFull Access
View options
View or Download as a PDF file.
PDFeReader
View online with eReader.
eReaderHTML Format
View this article in HTML Format.
HTML Format