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. Logics in Artificial Intelligence, LNCS 3229, 2004
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. Lecture Notes in Computer Science 3476, June 2006
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. 1st International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2002), 15-19 July 2002
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. Advances in Agent Communication, 2004
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. 2nd International Joint Conference on Autonomous Agents and Multi-Agents Systems (AAMAS 2003), 11-14 July 2003
- Verifiable Multi-agent Programs. Lecture Notes in Computer Science 3067, 2004
- Verifying Multi-agent Programs by Model Checking. Autonomous Agents and Multi-Agent Systems 12(2), 2006
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. Annals of Mathemathics and Artificial Intelligence 51(2-4), 2007
