Skip to main content

2020 | OriginalPaper | Buchkapitel

A Planning Approach Based on APTL

verfasst von : Haiyang Wang, Yao Liu

Erschienen in: Structured Object-Oriented Formal Language and Method

Verlag: Springer International Publishing

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

search-config
loading …

Abstract

This paper proposes a path planning approach for multi-agent systems (MASs) with Alternating Projection Temporal Logic (APTL). Our approach aims to calculate a path efficiently which satisfies specific properties in a MAS. The MAS is formalized in an interpreted system, then symbolically represented, and properties of paths are expressed by APTL formulas. We implement a robotic soccer game in order to illustrate the availability of this approach, actions and strategies of each robot are described in detail in interpreted system. The toolkit MCMAS_APTL2 has been developed, where we just enter an APTL formula of specific properties and the model of the robotic soccer game into the toolkit, then a path satisfies the formula is calculated and provided.

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!

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!

Literatur
2.
Zurück zum Zitat Kim, D.H., Kim, Y.J., Kim, K.C., Kim, J.H., Vadakkepat, P.: Vector field based path planning and petri-net based role selection mechanism with Q-learning for the soccer robot system. Intell. Autom. Soft Comput. 6(1), 75–87 (2000)CrossRef Kim, D.H., Kim, Y.J., Kim, K.C., Kim, J.H., Vadakkepat, P.: Vector field based path planning and petri-net based role selection mechanism with Q-learning for the soccer robot system. Intell. Autom. Soft Comput. 6(1), 75–87 (2000)CrossRef
3.
Zurück zum Zitat Xu, L., Tian, C., Duan, Z., Hongwei, D.: Planning with spatio-temporal search control knowledge. IEEE Trans. Knowl. Data Eng. 30(10), 1915–1928 (2018)CrossRef Xu, L., Tian, C., Duan, Z., Hongwei, D.: Planning with spatio-temporal search control knowledge. IEEE Trans. Knowl. Data Eng. 30(10), 1915–1928 (2018)CrossRef
4.
Zurück zum Zitat Wang, H., Duan, Z., Tian, C.: Model checking multi-agent systems with APTL. Ad Hoc Sens. Wirel. Netw. 37(1–4), 35–52 (2017) Wang, H., Duan, Z., Tian, C.: Model checking multi-agent systems with APTL. Ad Hoc Sens. Wirel. Netw. 37(1–4), 35–52 (2017)
6.
Zurück zum Zitat Lomuscio Alessio, Q., Hongyang, R.F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 173(9–10), 1–22 (2015) Lomuscio Alessio, Q., Hongyang, R.F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 173(9–10), 1–22 (2015)
7.
Zurück zum Zitat Lomuscio, A., Michaliszyn, J.: Model checking multi-agent systems against epistemic HS specifications with regular expressions. In: Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning, KR 2016, Cape Town, South Africa, 25–29 April 2016, pp. 298–308 (2016) Lomuscio, A., Michaliszyn, J.: Model checking multi-agent systems against epistemic HS specifications with regular expressions. In: Proceedings of the Fifteenth International Conference on Principles of Knowledge Representation and Reasoning, KR 2016, Cape Town, South Africa, 25–29 April 2016, pp. 298–308 (2016)
8.
Zurück zum Zitat Duan, Z., Tian, C., Zhang, N.: A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. 609, 544–560 (2016)MathSciNetCrossRef Duan, Z., Tian, C., Zhang, N.: A canonical form based decision procedure and model checking approach for propositional projection temporal logic. Theor. Comput. Sci. 609, 544–560 (2016)MathSciNetCrossRef
9.
Zurück zum Zitat Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theor. Comput. Sci. 497, 84–107 (2013)MathSciNetCrossRef Duan, Z., Zhang, N., Koutny, M.: A complete proof system for propositional projection temporal logic. Theor. Comput. Sci. 497, 84–107 (2013)MathSciNetCrossRef
10.
Zurück zum Zitat Wang, M., Tian, C., Zhang, N., Duan, Z.: Verifying full regular temporal properties of programs via dynamic program execution. TR 68(3), 1101–1116 (2019) Wang, M., Tian, C., Zhang, N., Duan, Z.: Verifying full regular temporal properties of programs via dynamic program execution. TR 68(3), 1101–1116 (2019)
11.
Zurück zum Zitat Cui, J., Duan, Z., Tian, C., Hongwei, D.: A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. Reliab. 67(2), 481–493 (2018)CrossRef Cui, J., Duan, Z., Tian, C., Hongwei, D.: A novel approach to modeling and verifying real-time systems for high reliability. IEEE Trans. Reliab. 67(2), 481–493 (2018)CrossRef
12.
Zurück zum Zitat Bin, Y., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89–99 (2018)CrossRef Bin, Y., Duan, Z., Tian, C., Zhang, N.: Verifying temporal properties of programs: a parallel approach. J. Parallel Distrib. Comput. 118, 89–99 (2018)CrossRef
13.
15.
Zurück zum Zitat Tian, C., Duan, Z.: Detecting spurious counterexamples efficiently in abstract model checking. In: ICSE, pp. 202–211 (2013) Tian, C., Duan, Z.: Detecting spurious counterexamples efficiently in abstract model checking. In: ICSE, pp. 202–211 (2013)
16.
Zurück zum Zitat Guarnizo, J.G., Mellado, M., Low, C.Y., Aziz, N.: Strategy model for multi-robot coordination in robotic soccer. Appl. Mech. Mater. 393, 592–597 (2013)CrossRef Guarnizo, J.G., Mellado, M., Low, C.Y., Aziz, N.: Strategy model for multi-robot coordination in robotic soccer. Appl. Mech. Mater. 393, 592–597 (2013)CrossRef
Metadaten
Titel
A Planning Approach Based on APTL
verfasst von
Haiyang Wang
Yao Liu
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-41418-4_9