Model checking of a mobile robots perpetual exploration algorithm

DOI10.1007/978-3-319-57708-1_12MaRDI QIDQ4989020zbMATH OpenOpenAlexFDO

Authors Ha Thi Thu Doan, François Bonnet, Kazuhiro Ogata

Publication date 20 May 2021

Published in Structured Object-Oriented Formal Language and Method (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-57708-1_12

zbMATH Keywords

automatic verificationMaudemobile robotsmodel checkingperpetual exploration

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40)

Recommendations

• Model checking of robot gathering
• Formal verification of mobile robot protocols
• Model checking MASL specification of distributed real-time systems
• The Maude LTL model checker
• scientific article; zbMATH DE number 1744967

Cited in

(8)

• Parameterized verification of algorithms for oblivious robots on a ring
• Embedded pattern formation by asynchronous robots without chirality
• Formal verification of mobile robot protocols
• Asynchronous arbitrary pattern formation: the effects of a rigorous approach
• Model checking of robot gathering
• Model checking algorithm based on ant colony swarm intelligence
• Squeezing streams and composition of self-stabilizing algorithms
• An environment for specifying and model checking mobile ring robot algorithms

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Model checking of a mobile robots perpetual exploration algorithm

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