Kripke modelling and verification of temporal specifications of a multiple UAV system

DOI10.1007/S10472-011-9270-XMaRDI QIDQ434449zbMATH OpenOpenAlexFDO

Authors Gopinadh Sirigineedi, Antonios Tsourdos, Brian White, Rafał Żbikowski

Publication date 10 July 2012

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10472-011-9270-x

zbMATH Keywords

model checkingformal verificationKripke modellingmulti-UAV systems

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Artificial intelligence for robotics (68T40) Automated systems (robots, etc.) in control theory (93C85) Temporal logic (03B44) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Formal modelling and verification of multi-robot systems specified with temporal logic
• Kripke modelling approaches of a multiple robots system with minimalist communication: A formal approach of choice
• A study of Kripke modeling of a multirobot syste for cooperative control
• Linear temporal logic vehicle routing with applications to multi-UAV mission planning
• Bounded model checking for deontic interpreted systems

Cites work

• scientific article; zbMATH DE number 438994 (Why is no real title available?)
• scientific article; zbMATH DE number 868107 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• scientific article; zbMATH DE number 2188051 (Why is no real title available?)
• A completeness theorem in modal logic
• A tabu search algorithm for the Min-Max \(k\)-Chinese postman problem
• Automatic support for verification of secure transactions in distributed environment using symbolic model checking
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Kripke modelling approaches of a multiple robots system with minimalist communication: A formal approach of choice
• Logic in Computer Science
• On Curves of Minimal Length with a Constraint on Average Curvature, and with Prescribed Initial and Terminal Positions and Tangents
• Verifying the IEEE 1394 fireWire tree identify protocol with SMV

Cited in

(2)

• Kripke modelling approaches of a multiple robots system with minimalist communication: A formal approach of choice
• Formal modelling and verification of multi-robot systems specified with temporal logic

Describes a project that uses

Uses Software

• SPIN

This page was built for publication: Kripke modelling and verification of temporal specifications of a multiple UAV system

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