An approach for specification and verification of multi-agent systems

 single agent. 
96 TRƯỜNG ĐẠI HỌC THỦ ĐÔ H NỘI 
 In the paper, we propose a method for the specification and verification of multiagent 
systems which number of agents are infinite. CafeOBJ is used as a tool for specifying 
agent’s actions and state space of the system. Theorem prover named CafeOBJ is also used 
to verify invariant properties of the system. 
4. THE PROPOSED METHOD 
 In multiagent systems, actions of each agent are autonomous. However, in some 
cases, the objectives of the system are only obtained by the interaction of agents; for 
example, the sharing resource in the system requires each agent must interact with others. 
In order to verify the combination of agent can obtain the system goals or not, we need to 
specify behaviors system by specifying the behaviors of agents. In this section, we propose 
the method to resolve the issues. Firstly, we present the method for specifying agents 
through specifying actions of agents. Next, the specification of MAS by specifying the 
state space of MAS will be described. In section 4.3, the invariant properties which are 
popular properties of MAS are defined. Finally, we propose a method to check whether the 
MAS satisfy the invariant properties or not in section 4.4. 
4.1. Specification of Agents 
 In MAS, an agent can be either acknowledged as an independent object that has an 
inference mechanism or it can be a member of a system that requires each agent must 
interact with others to obtain the system goals. In general level, the agent receives 
information from the environment and information from other agents through its sensor. In 
order to interact with other agents and the environment, an agent selects one of its actions. 
Which action should be selected depends on information about the environment and the 
current state of the system. 
 Let Aid be a set of indexes of agents and Sys be the state space of MAS. Each agent 
aihas a finite set of n actions such as a i1 , a i2 , a i3 a in . The specification of agents is 
performed by specification of its actions. Each action a ij is defined as follows. 
 Definition 1 . (Agent’s action). An action a ij is defined as a function which maps Aid × 
Sys to Sys (i.e., a ij : Aid × Sys → Sys). 
 Note 1. We use a ij (i, s) where i ∈ Aid, s ∈ Sys to denote that the agent a i performs the 
action a ij at the state s of system. The impact of this action can make the system go to the 
next state s’ = a ij (i, s) or remain the current state s. 
TẠP CHÍ KHOA HỌC −−− SỐ 18/2017 97 
 In order to know whenever the action can be performed or not and therefore, the 
system will go to another state or not, we define function caij as follows: 
 Definition 2 . (Condition of agent’s action). A condition of agent’s action caij 
is defined as a function which maps Aid × Sys to {true, false} (i.e., caij : Aid × Sys → 
{true, false). 
 Note 2. We use c aij (i, s) where i ∈ Aid, s ∈ Sys to denote that the agent a i performs 
the action a ij at the state s of system successfully or not and therefore, the system will go to 
the next state s’ or not. If c aij (i, s) = true, action a ij (i, s) is performed successfully and the 
system will go to the next state s. Otherwise, if c aij (i, s) = false, agent a i does not perform 
action a ij successfully, the state of system is still s. 
4.2. Specification of State Space of MAS 
 In MAS, number of agents often change during the development process of the 
system, then we do not know exactly the number of agents in MAS. Thus, in this paper, we 
consider the state space that is obtained by the impaction of agents’ actions is infinite. The 
state space of MAS is a combination of the initial state and the next states. Let init be the 
initial state and s be the state of MAS. At each state s ∈ Sys, the system will go to the next 
state s’ = a ij (i, s) if one of agents a i(i ∈ Aid) performs successfully action a ij at state s. The 
state space of MAS can be specified recursively: 
 Sys = {init} ∪∪∪ {a ij (i,s) | i ∈∈∈ Aid, s ∈∈∈ Sys, j ∈∈∈ [1.. n]} 
4.3. Specification of Invariant Properties 
 A MAS which is developed has to satisfy some required properties. Before a system is 
deployed, required properties need to be verified. In this paper, we only focus on 
specification and verification of invariant required properties. These are common 
properties of systems in general and MASs in particular. An invariant property is defined 
as follows: 
 Definition 3. (Invariant property). An invariant property inv is defined as a function 
which maps Sys to {true, false} (i.e., inv: Sys → {true, false}). 
 Note 3. We use inv(s) = true where s ∈ Sys to denote that the system has to satisfy 
with all states of system. The verification of correctness of invariant property inv is 
equivalent to verify that with every state s (s ∈ Sys) then inv(s) = true. 
98 TRƯỜNG ĐẠI HỌC THỦ ĐÔ H NỘI 
4.4. Verification of Multiagent Systems 
 Currently, software testing [26] has been recognized as the most popular solution for 
detecting errors/mistakes of systems. However, testing has been done after implementing 
phase in the life cycle of software development then we cannot apply testing for checking 
the correctness of the design phase. In order to check the correctness of the design phase, 
formal verification is currently widely applied. In this verification method, model checking 
and theorem proving are two methods that have been using mostly. Model checking which 
formally describes behaviors of the system and a required property is given into a model 
checker for verifying correctness of the design of the system. However, this model is 
difficult to use for analyzing the programs which contain complex data type like trees, lists, 
recursive definitions [27]. Moreover, the number of states of the model is finite, then we 
cannot apply this model for verifying the system that a number of states are infinite. In 
MAS, the number of agents often changes during the system development process. In 
general, we can assume that the number of agents is unknown. As a result, we cannot apply 
model checking to verify the correctness of MAS. 
 Base on theorem proving described in section 2.2 and induction mathematical idea, we 
propose a verified method that applied to prove the correctness of MAS that the state space 
is specified recursively and number of agents is infinite. Suppose that the system has some 
invariant properties and we have to verify that the system satisfies all invariant properties. 
Figure 1 presents the proven process for verification of an invariant property of the system. 
In this figure, the verification of an invariant property has been done by verifying in the 
base case and induction case. In the base case, we check the property inv is satisfied at 
initial state or not ( inv(init) = true ? ). If true, we move to prove inv in the inductive step. 
Otherwise, if inv(init) = false , we can conclude that the system does not satisfy with 
property inv . In inductive case, suppose that the system satisfies with property inv at state 
s, we must prove that the system also satisfies with property inv at all the next states s’. 
The next state s’ is the state of the system that is obtained by an action of any agent 
performs successfully its action at state s. If property inv is satisfied at the next states of s 
then we can conclude that the system satisfies with property inv . Otherwise, the system 
does not satisfy with property inv . In the process of verifying invariant properties of MAS, 
the obtained results are neither true nor false at some next states of the system. And 
therefore, we cannot know that the system satisfies or not invariant properties. In these 
cases, we need providing some lemmas to prove that inv(s) returns true. These lemmas are 
based on attributes of system that relate to inv . Before being applied, these lemmas need to 
be verified as well as properties of the system. 
TẠP CHÍ KHOA HỌC −−− SỐ 18/2017 99 
 Base case
 false Inv is not 
 inv(init ) = true satisfied
 true
 Induction hypothesis:
 inv(s) = true | s Sys
 Induction case
 Neither true 
 Inv is not 
 Add lemmas nor false inv(s’) = true false
 satisfied
 s’ =aij(i,s)
 true
 inv is satisfied
 Fig. 1. Verification process of invariant property of MAS. 
5. CONCLUSION AND FUTURE WORKS 
 In this paper, we proposed a method for the specification and verification of multi
agent systems which state space is infinite. With this issue, model checking cannot be 
applied to resolve. In the proposed method, we used algebraic language for specifying 
behaviors of agents, behaviors of the system and invariant required properties. In the 
specification of behaviors of agents, actions of agents were specified. In order to know 
when an agent performs its action successfully, we also defined conditional action 
function. Based on these specifications, state space of MAS was specified recursively as a 
combination of initial state and the next states that are obtained when any agent performs 
successful its actions. Required invariant properties of the system also were defined as the 
properties that the system has to satisfy at all states of the system. After specifying MAS, 
we presented the method for verification of the system. The proposed method is a theorem 
prover named CafeOBJ has been done by checking invariant property is satisfied at initial 
state and the next states. 
 As future work, we propose to realize the proposed method by specifying and 
verifying Airline Ticket Booking system that number of booking agents is unknown. We 
100 TRƯỜNG ĐẠI HỌC THỦ ĐÔ H NỘI 
also intend to combine model checking and theorem proving for specifying and verifying 
multiagent systems. For example, model checking is used for modeling behaviors of 
booking agents and verifying them. This means that the correctness of the specification of 
the system will be verified. The invariant required properties of the system will be verified 
by theorem proving. This combination will provide benefits in term of automation and can 
be used on large systems. Although invariant properties are common properties of the 
system in general, several properties are not invariant, then it is necessary to research how 
to translate the other properties into invariant properties. For example, based on semantics 
of the properties we will translate the properties into invariant properties. This will increase 
the applicability of the proposed method. 
 REFERENCE 
1. Bergenti, F., Gleizes, M.P., Zambonelli, F., et al (2004), “Methodologies and Software 
 Engineering for Agent Systems” . The agent – Oriented Software Engineering Handbook : 
 pp.1022. 
2. Bernon, C., Cossentino, M., Gleizes., M.P., Turci, P., Zambonelli, F. (2004), “ A study of 
 some MultiAgent MetaModels” . The Fifth International Workshop on AgentOriented 
 Software Engineering : pp.6277. 
3. B. HendersonSellers and P. Giorgini, et al. (2005), “AgentOriented Methodologies”: pp.136172. 
4. Alex L. G. Hayzelden and Rachel A. Bourne. (2001), “Agent Technology for Communication 
 Infrastructures ”: pp.254260. 
5. K. Sycara (1998), “Multiagent Systems”. AI Magazine , 19(2): pp.7992. 
6. G. Weiss (1999), “Multiagent Systems: a Modern Approach to Distributed Artificial 
 Intelligence”.pp.259265. 
7. M. Wooldridge (2002), “An Introduction to MultiAgent Systems”. pp.1320. 
8. Rajkumar Buyya (2012), “Software Life Cycle and Models” Available from: 
9. E. M. Clarke (2001), “Model Checking”. Handbook of automated reasoning : pp.1635 – 1790. 
10. J. Kramer and J. Magee (2006), “Concurrency: State Models & Java Programming”: pp.610. 
11. CafeOBJ Home Page (2012), Avaiable from:  
12. Kokichi Futatsugi, A.T. Nakagawa, and T. Tamai (2000), “CAFE: An IndustrialStrength 
 Algebraic Formal Method”: pp.110. 
13. Razvan Diaconescu and Kokich Futatsugi (1998), “CafeOBJ Report, The language, Proof 
 Techniques, and Methodologies for ObjectOriented Algebraic Specification”: pp.131. 
14. Michael Wooldridge (2012), “An Introduction to MultiAgent Systems”: pp.1938. 
15. K. Futatsugi, J. Goguen, J.P. Jouannaud, and J. Meseguer (1985), “Principles of OBJ2. Proc. 
 12th ACM Symposium on Principles of Programming Languages” , ACM: pp.52–66. 
16. K. Futatsugi, J. Goguen, JP.Jouannaud, J. Meseguer and T. Winkler (2000), “Introducing 
 OBJ”: pp.3167. 
TẠP CHÍ KHOA HỌC −−− SỐ 18/2017 101 
17. Joseph Goguen and R˘azvan Diaconescu (1994), “Towards an algebraic semantics for the 
 object paradigm” , Lecture Notes in Computer Science. Springer : pp.134. 
18. Joseph Goguen and Grant Malcolm (2012), “A hidden agenda”. Available from: 
 cse.ucsd.edu/users/goguen/pubs/index.html 
19. Vishnu Kotrajaras (2003), “Towards an AgentSearchable Software Component Using 
 CafeOBJ Specification and Semantic Web”, Satellite Workshop of the FM: pp.187210. 
20. Shuusaku Iida (2012), “Behavioural specification of a counter using CafeOBJ”, Available 
 from  
21. Michael Wooldridge, Michael Fisher, MarcPhilippe Huget, and Simon Parsons (2002), 
 “Model checking multiagent systems with MABLE” , ACM: pp.952–959. 
22. Gerard J. Holzmann (2003), “The SPIN Model Checker”: pp.3372. 
23. Rafael H. Bordini, Michael Fisher, Willem Visser, and Michael Wooldridge (2006), 
 “Verifying multiagent programs by model checking”. Journal of Autonomous Agents and 
 MultiAgent Systems: pp.239–256. 
24. Louise A. Dennis, Berndt Farwer, Rafael H. Bordini, and Michael Fisher (2008), “A flexible 
 framework for verifying agent programs”, Autonomous Agents and MultiAgent Systems: 
 pp.1303–1306. 
25. N. Alechina, M. Dastani, F. Khan, B. Logan and J.J. Ch. Meyer (2010), “Using Theorem 
 Proving to Verify Properties of Agent Programs”. Springer: pp.133. 
26. Ron Patton (2005), “Software testing”, pp.137. 
27. Kaufmann, M., Moore, J.S (2004), “Some Key Research Problems in Automated Theorem 
 Proving for Hardware and Software Verification”. Spanish Royal Academy of Science 
 (RAMSAC) : pp.181–196. 
 PHƯƠNG PHÁP ĐC T VÀ KIM CHNG CÁC H ĐA TÁC T 
 Tóm tttttt: Các h thng ña tác t (MASs) ñã ñưc công nhn là phương pháp tip cn hin 
 ñi cho phát trin phn mm, trong ñó mi thành phn phn mm là ñc lp và có tính t 
 tr như tác t. Tuy nhiên, làm th nào ñ ñm bo tính chính xác ca thit k trưc khi thi 
 hành vn còn là mt vn ñ m và thú v. Mc tiêu ca bài báo này là ñ xut mt 
 phương pháp ñc t và kim chng các h thng ña tác t ñ gii quyt vn ñ ñưc mô 
 t. Trong phương pháp này, s lưng tác t ca các h MAS là vô hn và do ñó không 
 gian trng thái ca h thng cũng vô hn. 
 TTTT kkhhóóaakhóa:khóa Đc t, kim chng, h ña tác t, thuyt chng minh, các thuc tính bt bin, 
 CafeOBJ.