DLTL - Dynamic Linear Temporal Logic

This logic provides a formalization of agent communicative actions in term of their effects and pre-conditions, enabling the representation of interaction protocols using permissions and commitments via temporal constraints.

• Verifying Communicating Agents by Model Checking in a Temporal Action Logic (paper in proceedings, 2004) — Laura Giordano, Alberto Martelli, Camilla Schwind

GLTL - Generalized Linear Temporal Logic

This logic enables the creation of statements about properties of system states as well as action labels on transitions between states. The semantics of GLTL is given in terms of infinite paths (called runs) of a Labeled Transition System (LTS). Runs are infinite sequences of states of the LTS.

• Modeling and Verification of Distributed Autonomous Agents Using Logic Programming (paper in proceedings, 2006) — L. Robert Pokorny, C. R. Ramakrishnan

MABLE

This is an imperative C-like language for the design and automatic verification of multiagent systems. Agents in MABLE are deigned using BDI structures. MABLE systems can be augmented using logic properties called claims concerning the overall status of the system.

• Model Checking Multi-Agent Systems with MABLE (paper in proceedings, 2002) — Michael J. Wooldridge, Michael Fisher, Marc-Philippe Huget, Simon Parsons

MABLE supports the definition of performative semantics to enrich the multiagent system with. This definitions add a set of pre- and post-conditions to communicative acts that the system is bound to satisfy whenever realizing that particular communication.

• Model Checking for ACL Compliance Verification (book chapter, 2004) — Marc-Philippe Huget, Michael J. Wooldridge

AgentSpeak(F)

This language is the restriction of AgentSpeak(L) to finite state systems by disallowing some features. With this approach it is possible to automatically verifiy if a multiagent system implemented in AgentSpeak(F) satisfies specifications expressed as BDI logic formulæ.

• Model Checking AgentSpeak (paper in proceedings, 2003) — Rafael H. Bordini, Michael Fisher, Carmen Pardavila, Michael J. Wooldridge

• Verifiable Multi-agent Programs (paper in proceedings, 2004) — Rafael H. Bordini, Michael Fisher, Willem Visser, Michael J. Wooldridge

• Verifying Multi-agent Programs by Model Checking (article in journal, 2006) — Rafael H. Bordini, Michael Fisher, Willem Visser, Michael J. Wooldridge

SLPN - Simple Logic Petri Nets

This is a new family of Petri nets expecially useful when modeling multiagent systems composed by AgentSpeak agents. The main feature of SLPNs is the specification of labels for the arcs in the net, representing the pre- and post-conditions of the transition.

• Model Checking Multi-agent systems with Logic Based Petri Nets (article in journal, 2007) — Tristan M. Behrens, Jurgen Dix

Environment