nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Case Study: Reachability and Scalability in a Unified Combat-Command-and-Control Model

verfasst von : Sergiy Bogomolov, Marcelo Forets, Kostiantyn Potomkin

Erschienen in: Reachability Problems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Reachability analysis computes an envelope encompassing the reachable states of a hybrid automaton within a given time horizon. It is known to be a computationally intensive task. In this case study paper, we consider the application of reachability analysis on a mathematical model unifying two key warfighting functions: Combat, and Command-and-Control (C2). Reachability here has a meaning of whether, given a range of initial combat forces and a C2 network and various uncertainties, one side can survive combat with intact forces while the adversary is diminished to zero. These are questions which arise in military Operations Research (OR). This paper is the first to utilize the notions of a hybrid automaton and reachability analysis in the area of OR. We explore the applicability and scalability of Taylor-model based reachability techniques in this domain. Our experiments demonstrate the potential of reachability analysis in the context of OR.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Reachability Set Generation Using Hybrid Relation Compatible Saturation

Nächstes Kapitel Qualitative Multi-objective Reachability for Ordered Branching MDPs

https://github.com/kpotomkin/ReachabilityBenchmarks.

JuliaReach. https://github.com/JuliaReach (2017)

Acebrón, J.A., Bonilla, L.L., Vicente, C.J.P., Ritort, F., Spigler, R.: The Kuramoto model: a simple paradigm for synchronization phenomena. Rev. Modern Phys. 77(1), 137 (2005)CrossRef

Ahern, R., Zuparic, M., Kalloniatis, A., Hoek, K.: Unifying warfighting functions in mathematical modelling: combat, Manoeuvre and C2. Submitted to Journal of the Operational research Society (JORS)

Althoff, M.: Reachability analysis and its application to the safety assessment of autonomous cars. Ph.D. thesis, Technische Universität München (2010)

Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, pp. 173–182. ACM (2013)

Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991-1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-57318-6_30CrossRef

Bak, S., Bogomolov, S., Henzinger, T.A., Johnson, T.T., Prakash, P.: Scalable static hybridization methods for analysis of nonlinear systems. In: 19th International Conference on Hybrid Systems: Computation and Control (HSCC 2016), pp. 155–164. ACM

Bansal, S., Chen, M., Herbert, S., Tomlin, C.J.: Hamilton-Jacobi reachability: a brief overview and recent advances. In: IEEE 56th Annual Conference on Decision and Control (CDC), pp. 2242–2253. IEEE (2017)

Benet, L., Sanders, D.: TaylorSeries.jl: Taylor expansions in one and several variables in Julia. J. Open Source Softw. 4, 1043 (2019)CrossRef

10.

Benet, L., Sanders, D.P.: JuliaDiff/TaylorSeries.jl, March 2019. https://doi.org/10.5281/zenodo.2601942

11.

Benet, L., Sanders, D.P.: JuliaIntervals/TaylorModels.jl, March 2019. https://doi.org/10.5281/zenodo.2613103

12.

Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Comput. 4(4), 361–369 (1998). https://doi.org/10.1023/A:1024467732637MathSciNetMATHCrossRef

13.

Bogomolov, S., et al.: Guided search for hybrid systems based on coarse-grained space abstractions. Int. J. Softw. Tools Tech. Trans. 18(4), 449–467 (2015). https://doi.org/10.1007/s10009-015-0393-yMathSciNetCrossRef

14.

Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., Schilling, C.: JuliaReach: a toolbox for set-based reachability. In: 22nd ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2019), pp. 39–44. ACM (2019)

15.

Bogomolov, S., Mitrohin, C., Podelski, A.: Composing reachability analyses of hybrid systems for safety and stability. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 67–81. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15643-4_7MATHCrossRef

16.

Bronski, J., deVille, L., Park, M.J.: Fully synchronous solutions and the synchronization phase transition for the finite-N Kuramoto model. Chaos 22(3), 033133 (2012)MathSciNetMATHCrossRef

17.

Bünger, F.: Shrink wrapping for Taylor models revisited. Numer. Algorithms 78(4), 1001–1017 (2017). https://doi.org/10.1007/s11075-017-0410-1MathSciNetMATHCrossRef

18.

Chen, X., Abraham, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: IEEE 33rd Real-Time Systems Symposium, pp. 183–192. IEEE (2012)

19.

Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_18CrossRef

20.

Chen, X., Sankaranarayanan, S.: Decomposed reachability analysis for nonlinear systems. In: IEEE Real-Time Systems Symposium (RTSS), pp. 13–24. IEEE (2016)

21.

Dekker, A., Taylor, R.: Synchronization properties of trees in the Kuramoto model. SIAM J. Appl. Dyn. Sys. 12(2), 596–617 (2013)MathSciNetMATHCrossRef

22.

D’silva, V., Kroening, D., Weissenbacher, G.: A survey of automated techniques for formal software verification. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(7), 1165–1178 (2008)CrossRef

23.

da Fonseca, J., Abud, C.: The Kuramoto model revisited. J. Stat. Mech: Theory Exp. 2018(10), 103204 (2018)MathSciNetMATHCrossRef

24.

Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30CrossRef

25.

Girard, A., Guernic, C.L.: Efficient reachability analysis for linear systems using support functions. IFAC Proc. Vol. 41, 8966–8971 (2008)CrossRef

26.

Gomez-Gardenes, J., Moreno, Y., Arenas, A.: Synchronizability determined by coupling strengths and topology on complex networks. Phys. Rev. E 75, 066106 (2007)MathSciNetCrossRef

27.

Gupta, A.: Formal hardware verification methods: a survey. Form Method Syst. Des. 1, 151–238 (1992). In: Computer-Aided Verification. pp. 5–92. Springer CrossRef

28.

Hasík, J.: Beyond the briefing: theoretical and practical problems in the works and legacy of John Boyd. Contemp. Secur. Policy 34(3), 583–599 (2013)CrossRef

29.

Hong, H., Choi, M.Y., Kim, B.J.: Synchronization on small-world networks. Phys. Rev. E 65(2), 026139 (2002)CrossRef

30.

Ichinomiya, T.: Frequency synchronization in a random oscillator network. Phys. Rev. E 70(2), 026116 (2004)CrossRef

31.

Immler, F., et al.: ARCH-COMP19 category report: Continuous and hybrid systems with nonlinear dynamics. In: ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systemsi, part of CPS-IoT Week 2019, Montreal, QC, Canada, pp. 41–61 (2019)

32.

Immler, F., et al.: ARCH-COMP19 category report: continuous and hybrid systems with nonlinear dynamics. EPiC Ser. Comput. 61, 41–61 (2019)CrossRef

33.

Joldes, M.M.: Rigorous polynomial approximations and applications. Ph.D. thesis (2011)

34.

Kalloniatis, A., Hoek, K., Zuparic, M.: Network synchronisation and next generation combat models - a dynamical systems approach. In: 86th Military Operations Research Society Symposium (2018)

35.

Kalloniatis, A., McLennan-Smith, T., Roberts, D.: Modelling distributed decision-making in command and control using stochastic network synchronisation. Eur. J. Oper. Res. (2020). https://doi.org/10.1016/j.ejor.2019.12.033MATHCrossRef

36.

Kuramoto, Y.: International Symposium on Mathematical Problems in Theoretical Physics. Lecture Notes in Physics, p. 420. Springer, Heidelberg (1975). https://doi.org/10.1007/BFb0013294CrossRef

37.

Kuramoto, Y.: Chemical Oscillations, Waves, and Turbulence. Courier Corporation (2003)

38.

Lanchester, F.W.: Aircraft in Warfare: The Dawn of the Fourth Arm. Constable limited (1916)

39.

Leavitt, H.J.: Some effects of certain communication patterns on group performance. J. Abnorm. Soc. Psychol. 46(1), 38–50 (1951)CrossRef

40.

Makino, K., Berz, M.: Taylor models and other validated functional inclusion methods. Int. J. Pure Appl. Math. 6, 239–316 (2003)MathSciNetMATH

41.

Meyer, P.J., Devonport, A., Arcak, M.: Tira: toolbox for interval reachability analysis. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control, pp. 224–229. ACM (2019)

42.

Mitchell, I.M.: Comparing forward and backward reachability as tools for safety analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 428–443. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71493-4_34CrossRef

43.

Morse, P., Kimball, G.: Methods of Operations Research. Massachusetts Institute of Technology (1951)

44.

Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: 12th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN 2006), p. 4. IEEE (2006)

45.

Osinga, F.: “Getting” a discourse on winning and losing: a primer on Boyd’s “theory of intellectual evolution”. Contemp. Secur. Policy 34(3), 603–624 (2013)CrossRef

46.

Pérez-Hernández, J.A., Benet, L.: Perezhz/taylorintegration.jl, February 2019. https://doi.org/10.5281/zenodo.2562353

47.

Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., Grosu, R.: XSpeed: accelerating reachability analysis on multi-core processors. In: Piterman, N. (ed.) HVC 2015. LNCS, vol. 9434, pp. 3–18. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-26287-1_1CrossRef

48.

Rogge, J.A., Aeyals, D.: Stability of phase locking in a ring of unidirectionally coupled oscillators. SIAM J. Appl. Dyn. Syst. 37, 11135–11148 (2004)MathSciNetMATH

49.

Rwth, X.C., Sankaranarayanan, S., Ábrahám, E.: Under-approximate flowpipes for non-linear continuous systems. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 59–66. IEEE (2014)

50.

Tam, J.H.: Application of Lanchester combat model in the Ardennes campaign. Nat. Resour. Model. 11(2), 95–116 (1998)MathSciNetCrossRef

Titel: Case Study: Reachability and Scalability in a Unified Combat-Command-and-Control Model
verfasst von: Sergiy Bogomolov
Marcelo Forets
Kostiantyn Potomkin
Verlag: Springer International Publishing
Buch: Reachability Problems
Print ISBN: 978-3-030-61738-7

Electronic ISBN: 978-3-030-61739-4

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-61739-4_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner