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

DOI10.1007/s10472-011-9270-xzbMath1242.68171OpenAlexW2095002986MaRDI QIDQ434449

Gopinadh Sirigineedi, Antonios Tsourdos, Rafał Żbikowski, Brian A. White

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

formal verificationmodel checkingKripke modellingmulti-UAV systems

Mathematics Subject Classification ID

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

Uses Software

• SPIN

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Verifying the IEEE 1394 fireWire tree identify protocol with SMV
• A tabu search algorithm for the Min-Max \(k\)-Chinese postman problem
• A completeness theorem in modal logic
• On Curves of Minimal Length with a Constraint on Average Curvature, and with Prescribed Initial and Terminal Positions and Tangents
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Logic in Computer Science
• Kripke modelling approaches of a multiple robots system with minimalist communication: A formal approach of choice

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