Formal verification of BDI agents

DOI10.1007/978-3-031-73887-6_20MaRDI QIDQ7007843zbMATH OpenFDO

Authors Thomas Wright, Louise A. Dennis, Jim Woodcock, Simon Foster

Publication date 25 March 2025

Full work available at URL https://doi.org/10.1007/978-3-031-73887-6_20

zbMATH Keywords

agent verificationBDIIsabelle/HOLmodel checkingtheorem provingZ-machines

Mathematics Subject Classification ID

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

Cites work

• A refinement strategy for Circus
• A UTP semantics for \textsf{Circus}
• Agent technology from a formal perspective.
• An axiomatic basis for computer programming
• Automation for interactive proof: first prototype
• Foundations of rational agency
• scientific article; zbMATH DE number 140411 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• scientific article; zbMATH DE number 1949606 (Why is no real title available?)
• scientific article; zbMATH DE number 2080001 (Why is no real title available?)
• scientific article; zbMATH DE number 2090152 (Why is no real title available?)
• scientific article; zbMATH DE number 7730622 (Why is no real title available?)
• Natural deduction as higher-order resolution
• Objects, Agents, and Features
• Specification and Verification of Multi-agent Systems
• The B-Book
• Unifying heterogeneous state-spaces with lenses
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Verification of heterogeneous multi-agent system using MCMAS
• Verifying time, memory and communication bounds in systems of reasoning agents

This page was built for publication: Formal verification of BDI agents

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