An environment for specifying and model checking mobile ring robot algorithms

DOI10.1007/978-3-030-34992-9_10MaRDI QIDQ6536330zbMATH OpenFDO

Authors Ha Thi Thu Doan, Adrián Riesco, Kazuhiro Ogata

Publication date 19 April 2024

Full work available at URL https://doi.org/10.1007/978-3-030-34992-9_10

zbMATH Keywords

distributed mobile robot systemformal verificationmodel checkingring discrete modelspecification environment

Mathematics Subject Classification ID

Distributed systems (68M14) Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40) Distributed algorithms (68W15)

Recommendations

• Model checking of a mobile robots perpetual exploration algorithm
• Model checking of robot gathering
• Parameterized verification of algorithms for oblivious robots on a ring
• Formal verification of mobile robot protocols
• High-level modelling of cooperative mobile robot systems

Cites work

• A unified approach for gathering and exclusive searching on rings under weak assumptions
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Certified universal gathering in \(\mathbb {R}^2\) for oblivious mobile robots
• Computing on rings by oblivious robots: a unified approach for different tasks
• Computing without communicating: ring exploration by asynchronous oblivious robots
• Exclusive perpetual ring exploration without chirality
• Formal verification of mobile robot protocols
• Gathering asynchronous oblivious mobile robots in a ring
• Gathering on rings under the look-compute-move model
• LATIN 2004: Theoretical Informatics
• Logic in Computer Science
• Mobile robots gathering algorithm with local weak multiplicity in rings
• Model checking of a mobile robots perpetual exploration algorithm
• Model checking of robot gathering
• Optimal deterministic ring exploration with oblivious asynchronous robots
• Optimal probabilistic ring exploration by semi-synchronous oblivious robots
• Ring exploration with myopic luminous robots
• Synchronous gathering without multiplicity detection: a certified algorithm

This page was built for publication: An environment for specifying and model checking mobile ring robot algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6536330)