×

Time-constrained temporal logic control of multi-affine systems. (English) Zbl 1302.93113

In the paper, the following problem is considered: Given a multi–affine control system and syntactically co–safe Linear Temporal Logic (LTL) formula over rectangular subregions of the state space, find a set of initial states for which there exists a control strategy such that all the trajectories of the closed–loop system satisfy the formula within a given bound. Syntactically co–safe LTL formulas can be used to describe finite horizon specification such as target reachability with obstacles avoidance: ”always avoid obstacle O until reaching target T”, sequencing constraints ”go to C and not go to A or B unless C was visited before”, and more complex temporal and Boolean combinations of these.
The authors describe in detail the control strategy based on deterministic Büchi automata. An iterative refinement procedure via a random optimization algorithm is proposed. Also two examples are given. Computational experiments can be performed using the authors’ Matlab program conPAS available for download from the webside hyness.bu.edu/software.

MSC:

93B52 Feedback control
93B05 Controllability
49K15 Optimality conditions for problems involving ordinary differential equations
68Q70 Algebraic theory of languages and automata
90C25 Convex programming

Software:

Matlab; conPAS
PDF BibTeX XML Cite
Full Text: DOI arXiv

References:

[1] Girard, A., Synthesis using approximately bisimilar abstractions: state-feedback controllers for safety specifications, (Hybrid Systems: Computation and Control, (2010), ACM), 111-120 · Zbl 1361.68147
[2] Kloetzer, M.; Belta, C., A fully automated framework for control of linear systems from temporal logic specifications, IEEE Transactions on Automatic Control, 53, 1, 287-297, (2008) · Zbl 1367.93202
[3] Tabuada, P.; Pappas, G., Linear time logic control of discrete-time linear systems, IEEE Transactions on Automatic Control, 51, 12, 1862-1877, (2006) · Zbl 1366.93413
[4] Yordanov, B.; Tumova, J.; Belta, C.; Cerna, I.; Barnat, J., Temporal logic control of discrete-time piecewise affine systems, IEEE Transactions on Automatic Control, 57, 6, 1491-1504, (2012) · Zbl 1369.93355
[5] H.K. Gazit, G. Fainekos, G.J. Pappas, Where’s Waldo? Sensor-based temporal logic motion planning, in: IEEE Conference on Robotics and Automation, Rome, Italy, 2007.
[6] T. Wongpiromsarn, U. Topcu, R.M. Murray, Receding horizon temporal logic planning for dynamical systems, in: IEEE Conf. on Decision and Control, Shanghai, China, 2009, pp. 5997-6004.
[7] A. Bhatia, L.E. Kavraki, M.Y. Vardi, Motion planning with hybrid dynamics and temporal goals, in: IEEE Conf. on Decision and Control, Atlanta, GA, 2010, pp. 1108-1115.
[8] Gol, E. A.; Lazar, M.; Belta, C., Language-guided controller synthesis for discrete-time linear systems, (Hybrid Systems: Computation and Control, (2012), ACM), 95-104 · Zbl 1361.68114
[9] Volterra, V., Fluctuations in the abundance of a species considered mathematically, Nature, 118, 558-560, (1926) · JFM 52.0453.03
[10] Lotka, A., Elements of physical biology, (1925), Dover Publications, Inc. New York · JFM 51.0416.06
[11] Nijmeijer, H.; van der Schaft, A., Nonlinear dynamical control systems, (1990), Springer-Verlag · Zbl 0701.93001
[12] C. Belta, On controlling aircraft and underwater vehicles, in: Proceedings of the IEEE International Conference on Robotics and Automation, ICRA, Vol. 5, New Orleans, LA, 2004, pp. 4905-4910.
[13] de Jong, H., Modeling and simulation of genetic regulatory systems, Journal of Computational Biology, 9, 1, 69-105, (2002)
[14] Belta, C.; Habets, L., Control of a class of nonlinear systems on rectangles, IEEE Transactions on Automatic Control, 51, 11, 1749-1759, (2006) · Zbl 1366.93278
[15] L. Habets, M. Kloetzer, C. Belta, Control of rectangular multi-affine hybrid systems, in: IEEE Conf. on Decision and Control, 2006, pp. 2619-2624.
[16] Abate, A.; D’Innocenzo, A.; Di Benedetto, M., Approximate abstractions of stochastic hybrid systems, IEEE Transactions on Automatic Control, 56, 11, 2688-2694, (2011) · Zbl 1368.93655
[17] A.A. Julius, A.K. Winn, Safety controller synthesis using human generated trajectories: nonlinear dynamics with feedback linearization and differential flatness, in: American Control Conference, 2012.
[18] Mazo, M.; Tabuada, P., Symbolic approximate time-optimal control, Systems and Control Letters, 60, 4, 256-263, (2011) · Zbl 1216.93052
[19] A. Girard, Synthesis using approximately bisimilar abstractions: time-optimal control problems, in: IEEE Conf. on Decision and Control, Atlanta, GA, 2010, pp. 5893-5898.
[20] E.A. Gol, C. Belta, Time-constrained temporal logic control of multi-affine systems, in: 4th IFAC Conference on Analysis and Design of Hybrid Systems, 2012, pp. 102-107.
[21] Kupferman, O.; Vardi, M. Y., Model checking of safety properties, Formal Methods in System Design, 19, 291-314, (2001) · Zbl 0995.68061
[22] Latvala, T., Efficient model checking of safety properties, (Model Checking Software. 10th International SPIN Workshop, (2003), Springer), 74-88 · Zbl 1023.68625
[23] Kloetzer, M.; Belta, C., Dealing with nondeterminism in symbolic control, (Hybrid Systems: Computation and Control, (2008), Springer-Verlag Berlin, Heidelberg), 287-300 · Zbl 1143.68488
[24] Wolfgang, T., Infinite games and verification, (Computer Aided Verification, (2002), Springer Berlin, Heidelberg), 58-65
[25] E. Asarin, O. Maler, As soon as possible: time optimal control for timed automata, in: HSCC’99, 1999, pp. 19-30. · Zbl 0952.93064
[26] Trelea, I. C., The particle swarm optimization algorithm: convergence analysis and parameter selection, Information Processing Letters, 317-325, (2003) · Zbl 1156.90463
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.