Dynamic Exploration of Multi-agent Systems with Periodic Timed Tasks

• Autorzy: Arcile Johan , Devillers Raymond , Klaudel Hanna

Identyfikatory

DOI

10.3233/FI-2020-1948

• Języki publikacji: EN

Abstrakty

EN

We formalise and study multi-agent timed models MAPTs (Multi-Agent with Periodic timed Tasks ), where each agent is associated with a regular timed schema upon which all possible actions of the agent rely. MAPTs allow for an accelerated semantics and a layered structure of the state space, so that it is possible to explore the latter dynamically and use heuristics to greatly reduce the computation time needed to address reachability problems. We use an available tool for the Petri net implementation of MAPTs, to explore the state space of autonomous vehicle systems. Then, we compare this exploration with timed automata-based approaches in terms of expressiveness of available queries and computation time.

Słowa kluczowe

EN

on-the-fly exploration; periodic behaviour; real time multi-agent systems

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2020
• Tom: Vol. 175, nr 1-4
• Strony: 59--95
• Opis fizyczny: Bibliogr. 27 poz., rys., tab.

Twórcy

autor

Arcile Johan

• IBISC, Univ Evry, Université Paris-Saclay, 91025, Evry, France

autor

Devillers Raymond

• Department of Informatics, ULB Bruxelles, Belgium

autor

Klaudel Hanna

• IBISC, Univ Evry, Université Paris-Saclay, 91025, Evry, France

Bibliografia

• [1] Katrakazas C, Quddus M, Chen WH, Deka L. Real-time motion planning methods for autonomous on road driving: State-of-the-art and future research directions. Transportation Research Part C: Emerging Technologies, 2015. 60:416-442. doi:https://doi.org/10.1016/j.trc.2015.09.011.
• [2] Kuwata Y, Teo J, Fiore G, Karaman S, Frazzoli E, How JP. Real-Time Motion Planning With Applications to Autonomous Urban Driving. IEEE Transactions on Control Systems Technology, 2009. 17(5):1105-1118. doi:10.1109/TCST.2008.2012116.
• [3] Furda A, Vlacic L. Enabling Safe Autonomous Driving in Real-World City Traffic Using Multiple Criteria Decision Making. IEEE Intelligent Transportation Systems Magazine, 2011. 3(1):4-17. doi: 10.1109/MITS.2011.940472.
• [4] Likhachev M, Ferguson D. Planning Long Dynamically Feasible Maneuvers for Autonomous Vehicles. The International Journal of Robotics Research, 2009. 28(8):933-945. doi:10.1177/0278364909340445.
• [5] Glaser S, Vanholme B, Mammar S, Gruyer D, Nouveliere L. Maneuver-Based Trajectory Planning for Highly Autonomous Vehicles on Real Road With Traffic and Driver Interaction. IEEE Transactions on Intelligent Transportation Systems, 2010. 11(3):589-606. doi:10.1109/TITS.2010.2046037.
• [6] Foughali M, Berthomieu B, Dal Zilio S, Ingrand F, Mallet A. Model Checking Real-Time Properties on the Functional Layer of Autonomous Robots. In: International Conference on Formal Engineering Methods (ICFEM 2016). Tokyo, Japan, 2016 URL https://hal.archives-ouvertes.fr/hal-01346080.
• [7] Kamali M, Dennis LA, McAree O, Fisher M, Veres SM. Formal verification of autonomous vehicle platooning. Science of Computer Programming, 2017. 148:88-106. Special issue on Automated Verification of Critical Systems (AVoCS 2015), doi.org/10.1016/j.scico.2017.05.006.
• [8] Quottrup MM, Bak T, Zamanabadi RI. Multi-robot planning : a timed automata approach. In: IEEE International Conference on Robotics and Automation, 2004. Proceedings. ICRA ’04. 2004, volume 5. 2004 pp. 4417-4422 Vol.5. doi:10.1109/ROBOT.2004.1302413.
• [9] O’Kelly M, Abbas H, Mangharam R. APEX : Autonomous Vehicle Plan Verification and Execution. In: SAE World Congress. 2016. doi:10.4271/2016-01-0019.
• [10] Arcile J, Devillers R, Klaudel H. VerifCar: a framework for modeling and model checking communicating autonomous vehicles. Journal of Autonomous Agents and Multi-Agent Systems, 2019. 33(3):353-381. doi:10.1007/s10458-019-09409-x.
• [11] Alur R, Dill D. Automata for Modelling Real-Time Systems. In: Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP’90), volume 443 of LNCS. Springer-Verlag, 1990 pp. 322-335. doi:10.1007/BFb0032042.
• [12] UPPAAL. http://www.uppaal.org/.
• [13] Lime D, Roux OH, Seidner C, Traonouez LM. Romeo: A Parametric Model-Checker for Petri Nets with Stopwatches. In: TACAS. Springer Berlin Heidelberg. 2009 pp. 54-57. ISBN:978-3-642-00768-2.
• [14] Berthomieu B, Ribet PO, Vernadat F. The tool TINA - Construction of abstract state spaces for Petri nets and time Petri nets. International Journal of Production Research, 2004. 42(14):2741-2756. doi: 10.1080/00207540412331312688.
• [15] Pommereau F. ZINC: a compiler for “any language”-coloured Petri nets. Technical report, IBISC, university of Evry / Paris-Saclay, 2018. URL https://hal.archives-ouvertes.fr/hal-01941485.
• [16] Vernadat F, Azéma P, Michel F. Covering step graph. In: Application and Theory of Petri Nets 1996. Springer Berlin Heidelberg. 1996 pp. 516-535. ISBN:978-3-540-68505-0.
• [17] Clarke E, Grumberg O, Minea M, Peled D. State space reduction using partial order reduction. International Journal on Software Tools for Technology Transfer, 1999. 2:279-287. doi:10.1007/s100090050035.
• [18] Berthomieu B, Vernadat F. State Class Constructions for Branching Analysis of Time Petri Nets. In: In TACAS’03. Springer-Verlag. 2003 p. 442-457. ISBN:3540008985.
• [19] Clarke E, Biere A, Raimi R, Zhu Y. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design, 2001. 19(1):7-34. doi:10.1023/A:1011276507260.
• [20] Biere A, Cimatti A, Clarke EM, Strichman O, Zhu Y, et al. Bounded model checking. Advances in computers, 2003. 58(11):117-148.
• [21] Penczek W, Lomuscio A. Verifying Epistemic Properties of multi-agent systems via model checking. Fundamenta Informaticae, 2003. 2(52):167-185.
• [22] Bhat G, Cleaveland R, Grumberg O. Efficient on-the-fly model checking for CTL. In: Proceedings of LiCS. 1995 pp. 388-397. doi:10.1109/LICS.1995.523273.
• [23] Ben-David S, Heyman T, Grumberg O, Schuster A. Scalable Distributed On-the-Fly Symbolic Model Checking. In: Formal Methods in Computer-Aided Design. Springer Berlin Heidelberg. 2000 pp. 427-441. ISBN:978-3-540-40922-9.
• [24] Arcile J. Conception, modélisation et vérification formelle d’un système temps-réel d’agents coopératifs: application aux véhicules autonomes communicants. Ph.D. thesis, Université Paris-Saclay, France; préparée à l’Université d’Evry-Val-d’Essonne: URL https://www.biblio.univ-evry.fr/theses/2019/2019SACLE029.pdf.
• [25] Jensen K. Coloured Petri Nets - Basic Concepts, Analysis Methods and Practical Use - Volume 1. EATCS Monographs on TCS. Springer, 1992. ISBN:978-3-662-06291-3, 978-3-662-06289-0.
• [26] Peterson JL. Petri Net Theory and the Modelling of Systems. Prentice Hall, 1981. ISBN:978-0-13-661983-3.
• [27] Arcile J. Sources of the MAPTs models and exploration algorithms. https://forge.ibisc.univ-evry.fr/jarcile/MAPTs/. Accessed: 2019-10-11.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2020).