Highlights

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.

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.

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.

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.

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 (articolo in atti, 2003) — Rafael H. Bordini, Michael Fisher, Carmen Pardavila, 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.

Ambiente