The linear logic language [6] is an executable language for modeling concurrent and resource sensitive systems based on the general purpose specification logical language Forum [15]. is a multiset-based logic combining features of extensions of logic programming languages like Prolog, e.g. goals with implication and universal quantification, with the notion of formulas as resources at the basis of linear logic. A -program is a collection of multi-conclusion clauses of the form:

where the 's are atomic formulas, and the linear disjunction corresponds to the head of the clause. Furthermore, (i.e., ) is a linear implication. Clauses of this kind consume the resources (formulas) they need in order to be applied in a resolution step.

provides a way to ``guard'' the application of a given clause. In the following extended type of clauses

the goal-formulas 's must be solved in order for the clause to be triggered.

Referring to step 3 of the CaseLP development method, can be used to specify all the three levels of modeling. At the MAS level, a specification can prove useful to check properties of the communication among agents (for instance deadlock detection). At the architecture level, a specification includes details on agent data structures, and rules to model the architecture engine. At the behavior level, specific architecture dependent rules are defined. At any level, a description can be used to observe the evolution of an agent or, by using backward analysis, to detect violations of the requirements of the specifications. In [1] a -based framework for MAS is defined. It is used to model MAS in which agents with heterogeneous architectures can co-exist.
Note that one of CaseLP aims is to provide a set of specification languages together with their associated compilers into the prototype implementation language. The MAS developer will pick up and use the most suitable or familiar ones among them. At present is a mandatory choice if a high-level specification of the system is needed. The adoption of other high-level specification languages in CaseLP, as alternatives to , is part of our future work.