An environment for specifying and model checking mobile ring robot algorithms

DOI10.1007/978-3-030-34992-9_10MaRDI QIDQ6536330zbMATHFDO

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

Publication date 19 April 2024

zbMATH Keywords

model checkingformal verificationspecification environmentdistributed mobile robot systemring discrete model

Mathematics Subject Classification ID

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

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)