Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 3/2022

02-05-2022 | General

Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns

Authors: Yanni Kouskoulas, T. J. Machado, Daniel Genin, Aurora Schmidt, Ivan Papusha, Joshua Brulé

Published in: International Journal on Software Tools for Technology Transfer | Issue 3/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present an approach to analyze the safety of asynchronous, independent, non-deterministic, turn-to-bearing horizontal maneuvers for two vehicles. Future turn rates, final bearings, and continuously varying ground speeds throughout the encounter are unknown but restricted to known ranges. We develop a library of formal proofs about turning kinematics and apply the library to create a formally verified timing computation. Additionally, we create a technique that evaluates future collision possibilities that is based on waves of position possibilities and relies on the timing computation. The result either determines that the encounter will be collision-free, or computes a safe overapproximation for when and where collisions may occur.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
2
There exist alternate expressions for this angle, but to our knowledge, the formulation in this paper is new.
 
Literature
1.
go back to reference Abhishek, A., Sood, H., Jeannin, J.B.: In: Formal verification of braking while swerving in automobiles. Association for computing machinery. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC ’20. Association for Computing Machinery, New York, NY, USA (2020) Abhishek, A., Sood, H., Jeannin, J.B.: In: Formal verification of braking while swerving in automobiles. Association for computing machinery. In: Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, HSCC ’20. Association for Computing Machinery, New York, NY, USA (2020)
2.
go back to reference Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRef Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRef
3.
go back to reference Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages, pp. 134–183. Springer (1975) Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Automata Theory and Formal Languages, pp. 134–183. Springer (1975)
5.
go back to reference Fotiou, I.A., Rostalski, P., Parrilo, P.A., Morari, M.: Parametric optimization and optimal control using algebraic geometry methods. Int. J. Control 79(11), 1340–1358 (2006)MathSciNetCrossRef Fotiou, I.A., Rostalski, P., Parrilo, P.A., Morari, M.: Parametric optimization and optimal control using algebraic geometry methods. Int. J. Control 79(11), 1340–1358 (2006)MathSciNetCrossRef
6.
go back to reference Genin, D., Papusha, I., Brulé, J., Young, T., Mullins, G., Kouskoulas, Y., Wu, R., Schmidt, A.: Formal verification of neural network controllers for collision-free flight. In: 14th International Workshop on Numerical Software Verification (NSV) (2021) Genin, D., Papusha, I., Brulé, J., Young, T., Mullins, G., Kouskoulas, Y., Wu, R., Schmidt, A.: Formal verification of neural network controllers for collision-free flight. In: 14th International Workshop on Numerical Software Verification (NSV) (2021)
7.
go back to reference Isaiah, P., Shima, T.: A task and motion planning algorithm for the Dubins travelling salesperson problem. IFAC Proc. Vol. 47(3), 9816–9821 (2014). (19th IFAC World Congress)CrossRef Isaiah, P., Shima, T.: A task and motion planning algorithm for the Dubins travelling salesperson problem. IFAC Proc. Vol. 47(3), 9816–9821 (2014). (19th IFAC World Congress)CrossRef
9.
go back to reference Jeyaraman, S., Tsourdos, A., Żbikowski, R., White, B.A.: Formal techniques for the modelling and validation of a co-operating uav team that uses dubins set for path planning. In: Proceedings of the 2005, American Control Conference, 2005, vol. 7, pp. 4690–4695 (2005) Jeyaraman, S., Tsourdos, A., Żbikowski, R., White, B.A.: Formal techniques for the modelling and validation of a co-operating uav team that uses dubins set for path planning. In: Proceedings of the 2005, American Control Conference, 2005, vol. 7, pp. 4690–4695 (2005)
10.
go back to reference Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving—8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, pp. 336–353. Springer (2017) Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving—8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, pp. 336–353. Springer (2017)
11.
go back to reference Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving—8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10499, pp. 336–353. Springer (2017) Kouskoulas, Y., Genin, D., Schmidt, A., Jeannin, J.: Formally verified safe vertical maneuvers for non-deterministic, accelerating aircraft dynamics. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) Interactive Theorem Proving—8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings, Lecture Notes in Computer Science, vol. 10499, pp. 336–353. Springer (2017)
12.
go back to reference Kouskoulas, Y., Machado, T.J., Genin, D.: Formally verified timing computation for non-deterministic horizontal turns during aircraft collision avoidance maneuvers. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems—25th International Conference, FMICS 2020, Vienna, Austria, September 2–3, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12327, pp. 113–129. Springer (2020) Kouskoulas, Y., Machado, T.J., Genin, D.: Formally verified timing computation for non-deterministic horizontal turns during aircraft collision avoidance maneuvers. In: ter Beek, M.H., Nickovic, D. (eds.) Formal Methods for Industrial Critical Systems—25th International Conference, FMICS 2020, Vienna, Austria, September 2–3, 2020, Proceedings, Lecture Notes in Computer Science, vol. 12327, pp. 113–129. Springer (2020)
13.
go back to reference Kouskoulas, Y., Schmidt, A., Jeannin, J.B., Genin, D., Lopez, J.: Provably safe controller synthesis using safety proofs as building blocks. In: IEEE 7th International Conference on Software Engineering Research and Innovation, CONISOFT 2019, October 23–25, 2019, Mexico City, Mexico, pp. 26–35 (2019) Kouskoulas, Y., Schmidt, A., Jeannin, J.B., Genin, D., Lopez, J.: Provably safe controller synthesis using safety proofs as building blocks. In: IEEE 7th International Conference on Software Engineering Research and Innovation, CONISOFT 2019, October 23–25, 2019, Mexico City, Mexico, pp. 26–35 (2019)
14.
go back to reference Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796–817 (2001)MathSciNetCrossRef Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM J. Optim. 11(3), 796–817 (2001)MathSciNetCrossRef
15.
go back to reference LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)CrossRef LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)CrossRef
16.
go back to reference Ma, X., Castanon, D.A.: Receding horizon planning for Dubins traveling salesman problems. In: Proceedings of the 45th IEEE Conference on Decision and Control, pp. 5453–5458 (2006) Ma, X., Castanon, D.A.: Receding horizon planning for Dubins traveling salesman problems. In: Proceedings of the 45th IEEE Conference on Decision and Control, pp. 5453–5458 (2006)
17.
go back to reference McGee, T.G., Hedrick, J.K.: Path planning and control for multiple point surveillance by an unmanned aircraft in wind. In: 2006 American Control Conference, pp. 4261–4266 (2006) McGee, T.G., Hedrick, J.K.: Path planning and control for multiple point surveillance by an unmanned aircraft in wind. In: 2006 American Control Conference, pp. 4261–4266 (2006)
19.
go back to reference Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)MathSciNetCrossRef Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003)MathSciNetCrossRef
22.
go back to reference Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: IEEE Conference on Decision and Control, vol. 1, pp. 741–746 (2002) Prajna, S., Papachristodoulou, A., Parrilo, P.A.: Introducing SOSTOOLS: a general purpose sum of squares programming solver. In: IEEE Conference on Decision and Control, vol. 1, pp. 741–746 (2002)
23.
go back to reference Song, X., Hu, S.: 2d path planning with Dubins-path-based A\(\star \) algorithm for a fixed-wing UAV. In: 3rd IEEE International Conference on Control Science and Systems Engineering (ICCSSE), Beijing, China, pp. 69–73 (2017) Song, X., Hu, S.: 2d path planning with Dubins-path-based A\(\star \) algorithm for a fixed-wing UAV. In: 3rd IEEE International Conference on Control Science and Systems Engineering (ICCSSE), Beijing, China, pp. 69–73 (2017)
25.
go back to reference Wu, A., How, J.: Guaranteed infinite horizon avoidance of unpredictable, dynamically constrained obstacles. Auton. Robots 32(3), 227–242 (2012) Wu, A., How, J.: Guaranteed infinite horizon avoidance of unpredictable, dynamically constrained obstacles. Auton. Robots 32(3), 227–242 (2012)
Metadata
Title
Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns
Authors
Yanni Kouskoulas
T. J. Machado
Daniel Genin
Aurora Schmidt
Ivan Papusha
Joshua Brulé
Publication date
02-05-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 3/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00654-2

Other articles of this Issue 3/2022

International Journal on Software Tools for Technology Transfer 3/2022 Go to the issue

Premium Partner