Printer Friendly

Formal Specification and Verification of Real-Time Multi-Agent Systems using Timed-Arc Petri Nets.


The term 'formal methods' is utilized to allude to any exercises that depend on mathematical representations of software which includes but not limited to formal software specification, transformational development, formal verification of programs. In [1] an agent has been defined as any computer software system which autonomously achieves its objective when placed in an environment. A high degree of dependability is expected from autonomous software agents. The main purpose of these agents is to interact with the dynamic environment and it is not possible to build an agent with all the world knowledge composed into it. Being autonomous agents they are expected to respond intelligently to unfamiliar situations. A real-time agent (RTAgent) can be described as an agent with tight time-line constraints. For such agents response within specific deadlines is important or they lose their usability. An example of these RTAgent's might be intrusion detection systems, online auction systems, quoting systems for stock markets. These autonomous agents by their working nature have bounded response time constraints. The formal specification and verification of these real-time multi-agent systems (RTMAS) in which agents communicate with each other to achieve their goals within deadline will be of great value for their correct functioning. For such systems executing a predefined representative test cases of the system cannot provide a high degree of reliability. Even if we do achieve a high degree of test case coverage, the chances of system failure are still high due to test scenarios that were never executed. When receiving the external stimuli, these agents try to perceive it according to their knowledge and any failure in this process might cause the agents to fail. Formal verification of embedded systems for attributes like timing, probability and cost is an active area of research [2]. In the past many time-extended models have been devised for the formal verification of real-time systems like timed automata [3-4]. The use of formal methods for automated verification of real-time and safety critical systems is highly desirable [5].

In this paper we show how these RTMAS's can be formally specified and verified with bounded time constraints. Previously many agent architectures have been proposed for these multi-agent systems. A unified Modeling Language and Architecture Description Language based framework for formal modelling of multi-agent systems has been proposed in [6]. For agent communication they used a service agent that accepts Knowledge Query Manipulation Language (KQML). In [7] Stanford Research Institute (SRI) have proposed an agent framework called open Agent Architecture (OAA) that used a language called Interagent communication Language (ICL) using a facilitator agent. However we will use the agent framework for RTMAS that has been proposed in [8]. Their agent framework incorporates the necessary expressiveness for QoS constraints among RTAgent's communication. We can specify the timeline constraints as QoS constraints in their framework. Formal verification of e-agent's communication has been examined in detail previously. In [9] verifiable semantics based on computational models was proposed. Giordano has used Dynamic LTL Logic for specifying and verifying agent communication properties in [10]. In DLTL we express the programs as regular expressions and specify the communicative actions as precondition laws, causal laws and constraints. The use of model checking for verification of e-agents has been discussed in [11] using Belief-Desire-Intention (BDI) attitudes. They used a new logic which was the composition of formal temporal evolution and formal BDI attitudes. A process algebra based approach for agent's communication was discussed in [12]. They established a link between mathematical models and biological systems. In [13] petri-nets have been used for the modelling of railway networks to ensure the safety and deadlock free requirements. In [14] two techniques of formal methods namely Z-notation and X-machine for the formal specification of multi-agent systems have been used with a dynamic behavior and structure. In [15] a new XML based language called MASDL has been proposed for the specification of multi-agent systems in coloured petri nets. Mutli-agent systems have been modelled in [16-18] using petri nets but not RTMAS. However the use of model checking to formally verify the RTMAS with bounded time response is a novel approach. Communication between agents will be specified using the RTMAS framework proposed in [8]. Their architecture provides QoS services for RTAgent's communication. We will integrate the bounded delay response requirements of agents as part of QoS services. For verification that agent's actions conforms to bounded delay response requirements will be formally represented as a validity problem. The validity problem will then be solved with the help of TAPAAL model checker. TAPAAL is a verification tool for extended timed-arc Petri nets with its own verification engine. We can create models of the system under consideration and perform automated verification using fragments of TCTL via transformation to timed automata [19].

The rest of this paper is divided as follows. In section 2 some preliminaries for notations and semantics of RTMAS framework, TAPAAL and Timed-Arc Petri Nets are given. Section 3 describes the formal specification of the actions of RTAgents. In section 4 verification of the agents is done through TAPAAL. Section 5 concludes the paper.


A few terminologies, mathematical and computational models have been described in this section that will be used in the rest of the discussion for the specification of the problem under analysis.

A. RTMAS framework

The RTMAS framework proposed in [8] is based on existing Common Object Request Broker Architecture (CORBA) architecture by adding a layer of RTAgent's services. Addition of these agent services allows the expression of QoS constraints in RTMAS while the baseline communication support is provided by ORB layers and CORBA services. In real-time multi-agent systems the agents can achieve their goals in diverse traces. Every trace will have an ideal and a worst case time constraint which forms an acceptable interval. Each real-time agent (RTAgent) has explicit set of problems that it has been configured to solve, these problems are called solvable and we can express an RTAgent as a set of solvables.

RTAgent = [S.sub.1], [S.sub.2],..., [S.sub.n] (1)

Every solvable is further divided into two parts namely an optimal result and an execution strategy. Optimal result depicts the ideal solution for that solvable and it is context dependent. Execution strategy is a set itself and it contains the different execution methods that can be used for the solution of the solvable.

[S.sub.l] = <O, ES > (2)

ES = {[es.sub.1], [es.sub.2],..., [es.sub.n]} (3)

Further each execution startegy consists of an execution time (ex), quality (q) and tradeoff value (tv). Execution time represents the time it will took to execute that ES. Quality is the ratio of strategy result to optimal result. The quality thus requires that we perform quantification of the results. Tradeoff value depicts the quantifiable loss in case an ES is removed for a solvable. For simplicity in our specification of RTAgent's communication we will ignore the q and tv.

[es.sub.i] = <ex, q, tv> (4)

In this model Request (R) is used to represent that an RTAgent has requested another RTAgent for some services it require. R can be expressed as

R = <A,V, I, D> (5)

Here A is the RTAgent to which a service has been requested. The task requested to be performed by V. I is the importance of the request which is context dependent. The deadline for the request is represented by D and it can be either a soft deadline or a firm deadline.

B. TAPAAL Model Checker

For verification of RTAgent's communication we will need the TAPAAL model checker. It uses Timed-Arc Petri Nets (TAPN) for the verification of the proposed system. Properties of interest are specified as a subset of TCTL. TCTL is real-time logic which is used for the specification of timed properties about systems. These properties include safety properties, invariant, bounded-delay response, liveness properties, time progress etc [20]. TAPN's are basically an extension of the regular Petri nets in which age of tokens are used to represent the time information. The arcs between places and transitions are labeled with time intervals that confine the age of tokens that move along the arcs.

C. Timed-Arc Petri Nets

A TAPN is a 7-tuple (P, T, IA, OA, c, i, Type) where P is a finite set of places. T is a finite set of transitions such that P [intersection] T = [empty set]. IA [??] P x T is a finite set of input arcs. OA [??] T x P is a finite set of output arcs. c: IA [right arrow] I assigns intervals to input arcs. i: P [right arrow] [I.sub.inv] assigns age invariants to places. IA [union] OA [right arrow] {Normal,Inhib} [union]{Transpor[t.sub.t] | i [member of] N} is a function assigning a type to all arcs such that

1. Type(a) = Inhib [??] a [member of] IA [and] c(a) = [0,00) (6)

2. Type(p, t) = Transpor[t.sub.t] [??] [there exists]!(t, p') [member of] OA.

Type(t, p') = Transpor[t.sub.l] (7)

3. Type(t, p') = Transpor[t.sub.l] [??]

!(p, t) [member of] IA.Type(p, t) = Transpor[t.sub.l] (8)

In a TAPN that is k-bounded we repreent a Token as an element from 1,2,..., k. A marking M is a pair (pl, v) where pl: {1,2,...,k} [right arrow] [P.sub.[perpendicular to]] is the placement function and v: {1,2,...,k} [right arrow] R [greater than or equal to] 0 is the age function. A transition t [member of] T is enabled by a set of tokens IN [??] {1,2,...,k} in a marking (pl, v) if

1. t = {pl(i)| i [member of] IN} (9)

2. v(i)[member of] c(pl(i),t) for all i [member of] IN (10)

3. Type(pl(i), t) = Transport [??]

v(i)[member of] i(move(pl, IN,t)(i)) for all i [member of] IN (11)

4. (pl(i),t)[member of] IA [??]

Type(pl(i),t) [not equal to] Inhib for all i [member of] {1,2,...,k} (12)

A transition t enabled in a marking (pl, v) by the set of tokens IN can fire, producing a marking

(move(pl, IN, t), [v.sup.R=0]) where (13)

R = {i [member of] IN | Type(pl(i), t) [not equal to] Transport} (14)

These formulation will be used in order to specify the actions of the communicating agents.


We will use the Stock Trading System (STS) as described in [8] for the specification of the problem. In this system we have multiple RTAgents communicating with each other for tasks like keeping track of stock prices, sales and purchase of stocks. Basically there are four types of agents which are UserAgent, BuySellAgent, QuotingAgent and TrendWatchingAgent. Human agent will communicate with UserAgent and inform it about its requirements like amount of money to spend, his stock preferences according to his previous experience, risk level etc. Additionally the UserAgent can coordinate with other agents so as to fulfill user's requirements. The QuotingAgent has the capability to get quote of the stocks from different markets. It can also monitor the stock for prices of different products so that the TrendWatchingAgent is informed in case of any event of interest in timely manner. other agents communicate with it when they need information on stock prices. one QuotingAgent can also communicate with each other in case a request for a quote came which one QuotingAgent cannot satisfy. The TrendWatchingAgent monitors the market for any trends of interest as per requirement. In a system we may have many TrendWatchingAgent's, each responsible for different trend. When a trend of interest occurs like a certain stock price decreased 100 points within some time unit then the TrendWatchingAgent notifies the human user. The actual sale/purchase of stocks is performed by the BuySellAgent. It can act autonomously or with the help of human user, whatever the system policy has been set. In this system the real-time nature stems up from the requirement of tight deadlines.

Complete model of the proposed system is shown in Figure2. In our case study we have four stock markets represented by <SM1, SM2, SM3, SM4>. One user agent which is <UA>. Two agent instances of each quoting agents, buy sell agent and trend watching agent represented by <QA1, QA2>, <BSA1, BSA2>, <TWA1, TWA2> respectively. Each stock market has different real-time constraints associated with it. SM1, SM2, SM3 and SM4 are refreshed after every 3,5,7 and 9 time units respectively, so their prices of different products are valid only for that interval. These deadlines are defined as constants in the tool represented as SM[1.sub.D], SM [2.sub.D], SM [3.sub.D], SM [4.sub.D]. QA1 can communicate with SM1 and SM2 only. Whereas QA2 can communicate with SM3 and SM4 only. BSA1 can perform transactions with SM1 and SM3 only. Whereas BSA2 can perform transactions with SM2 and SM4 only. TWA1 and TWA2 both are responsible for monitoring of all stock markets so that whenever there is an increase or decrease in stock index of certain points in these stocks markets, it notifies the UA which in turn notifies the user. Location LU represents the LostUpdates. These are the updates which were not delivered to their specific QA within the deadline and hence were lost. We have four checkpoints namely CH1, CH2, CH3, CH4 which make use of the deadline intervals to ensure that only updates with valid deadlines are forwarded to QA. Each SM thus has the template as shown in Figure 1.

An update is only forwarded from any SM if it meets the deadline for that SM specified as [SM.sub.D]. The use of transport arc preserves the age of tokens so that the UA will ultimately receive the updates without an intermediate delay during the trace. In our model we are more concerned with requests of RTAgents and their deadline than the multiple ways of achieving the goal so we will integrate the ex directly into the requests assuming that there is a single solvable for each request. In case of coloured petri-nets user defined colour sets can be used to assign semantics for each solvable. Requests by different agents according to RTMAS framework are specified below.

[R.sub.SM1] = <QA1, SM_UPDATES, HIGH,3> (15)

[R.sub.SM2] = <QA1, SM_UPDATES, HIGH,5> (16)

[R.sub.SM3] = <QA2, SM_UPDATES, HIGH,7> (17)

[R.sub.SM4] = <QA2, SM_UPDATES, HIGH,9> (18)

[R.sub.QA1] = <TWA1, SM_UPDATES, HIGH,0> (19)

[R.sub.QA1] = <TWA2, SM_UPDATES, HIGH,0> (20)

[R.sub.QA1] = <UA, SM_UPDATES, HIGH,0> (21)

[R.sub.QA2] = <TWA1, SM_UPDATES, HIGH,0> (22)

[R.sub.QA2] = <TWA2, SM_UPDATES, HIGH,0> (23)

[R.sub.QA2] = <UA, SM_UPDATES, HIGH,0> (24)

[R.sub.BSA1] = <SM1, SM TRANSACTION, HIGH,0> (25)

[R.sub.BSA1] = <SM 3, SM TRANSACTION, HIGH,0> (26)

[R.sub.BSA2] = <SM 2, SM TRANSACTION, HIGH,0> (27)

[R.sub.BSA2] = <SM4, SM_TRANSACTION, HIGH,0> (28)

[R.sub.TWA1] = <UA,SM_TREND_ALERT,HIGH,0> (29)

[R.sub.TWA2] = <UA,SM_TREND_ALERT,HIGH,0> (30)

[R.sub.UA] = <BSA1, SM_TRANSACTION_ALERT, LOW, [0-[infinity]]> (31)

[R.sub.UA] = <BSA2, SM_TRANSACTION_ALERT, LOW, [0-[infinity]]> (32)

We have two levels of request importance namely I = {LOW, HIGH}. HIGH represents that we have a specified deadline for the transition within which the event should occur whereas LOW implies the spontaneous events. In our system the spontaneous events will be the buying and selling of stocks as per user direction. In a real-time system there might be some actions which have marginalized deadlines. In our system deadlines represent the age of tokens. A deadline of 0 implies an urgent transition. No time delay can occur in case of urgent transitions. There are three type of requests which are SM_UPDATES, SM_TRANSACTION, SM_TREND_ALERT. All the requests have tight deadlines except the requests generated by UA for purchasing/selling of stocks. The user can initiate the request at anytime.


TAPN is mostly used for the verification of three types of properties of interest. These are reachability, boundedness and liveness. Reachability is used for tracking of dead state i-e state which is not reachable from any other states. Boundedness ensures that our system will never use more than k amount of tokens. Liveness finds put if there will be a state where our system will be deadlocked. For verification of our system we had to create additional states. Goal_SM1, Goal_SM2, Goal_SM3, Goal_SM4, Goal_TWA1, Goal_TWA2, Goal_BSA1 and Goal_BSA2 represents such states which are not part of our STS. Figure 3 show a truncated model of SMS with these goals. Table 1 contains the properties that needs to be verified for our STS. The properties have been specified using AF, AG, EG, and EF fragments of TCTL via translations to timed automata. A quick look reveals that our system is not safe as it is not 1-bounded. Provision of proper time delays will ensure that the system never will never go into a deadlock state. All the SM's have been specified such that once a SM is enabled it will continuously remain enabled. The model checker not only reports whether a property is satisfied or not but also provides the trace of satisfiability and number of tokens utilized at each place. Due to increasing complexity of RTMAS a proper abstracted model of the system might provide useful insights before the system is actually engineered.

Due to succinctness we will only show the trace of property satisfaction and k-boundedness for the query "Are all the stock markets reachable?" in Table 2. The rest of the queries can be analyzed in the same way. Count represent the number of times a particular transition was enabled. Transitions with highest number of counts are mostly urgent. MaxTokens are the tokens that were utilized in a place during the verification of query. The STS.LU has unknown as max tokens which means this place is a sink place and number of tokens will continue to grow in it. This is exactly what the place LU has been designed for so that all the updates which were not delivered within time will go there. It should be noted that the trace is one of the many possible traces and not the fastest one.


In this paper we have shown how actions of communicating agents can be specified in TAPN's. We formally specified and verified the Stock Market System based on RTMAS framework using TAPN's. The model was verified used AF, AG, EG, and EF fragments of TCTL via translations to timed automata. TAPN's have been used for intuitive modeling and verification of real-time systems in the past to ensure their predictability. Multi-agent systems are seen as a key enabling technology for the future ecommerce products and they have been used to model critical components of large number of distributed applications in diverse areas of real life like business process management, distributed computing, supply chain management, workforce management, e-health care and knowledge discovery. To ensure a high degree of reliability and predictability of these systems we need formal verification for them. This is evident by the difficulty to achieve good test case coverage for a system of reasonable size. We have specified real-time requirements of the system using transition intervals and token's age. We used TAPAAL for the verification of properties of RTMAS. The technique can be used to specify and verify the properties of any number of agents. The major advantage of our approach is that it provides future directions for integrating timed petri nets and agent communication as a flexible and powerful tool for modelling of complex real-time system. Formal verification will help to prove the correctness of the system being modelled which in turn will increase the confidence in the correctness of the system. our future work will focus on using Timed coloured Petri-Nets for the formal modelling of self adaptive RTMAS.


[1] N. R. Jennings, K. Sycara, M. Wooldridge, "A roadmap of agent research and development," Autonomous agents and multi-agent systems, vol. 1, no. 1, pp. 7-38, 1998. [Online]. Available:

[2] E. Sikora, B. Tenbergen, K. Pohl, "Industry needs and research directions in requirements engineering for embedded systems," Requirements Engineering, vol. 17, no. 1, pp. 57-78, 2012. [online]. Available:

[3] R. Alur, A. Itai, R. P. Kurshan, M. Yannakakis, "Timing verification by successive approximation," Information and Computation, vol. 118, no. 1, pp. 142-157, 1995. [Online]. Available:

[4] R. Alur, D. L. Dill, "A theory of timed automata," Theoretical computer science, vol. 126, no. 2, pp. 183-235, 1994. [online]. Available:

[5] J. Bowen, V. Stavridou, "Safety-critical systems, formal methods and standards," Software Engineering Journal, vol. 8, no. 4, pp. 189-209, 1993. [online]. Available:

[6] S. Park, V. Sugumaran, "Designing multi-agent systems: a framework and application," Expert Systems with Applications, vol. 28, no. 2, pp. 259-271, 2005. [online]. Available:

[7] D. L. Martin, A. J. Cheyer, D. B. Moran, "The open agent architecture: A framework for building distributed software systems," Applied Artificial Intelligence, vol. 13, no. 1-2, pp. 91-128, 1999. [online]. Available:

[8] L. C. DiPippo, V. F. Wolfe, L. Nair, E. Hodys, O. Uvarov, "A realtime multi-agent system architecture for e-commerce applications", pp. 357-364, IEEE, 2001.

[9] M. Wooldridge, "Semantic issues in the verification of agent communication languages," Autonomous agents and multi-agent systems, vol. 3, no. 1, pp. 9-31, 2000. [online]. Available:

[10] L. Giordano, A. Martelli, C. Schwind, "Specifying and verifying interaction protocols in a temporal action logic," Journal of Applied Logic, vol. 5, no. 2. pp. 214-234, 2007. [online]. Available:

[11] M. Benerecetti, F. Giunchiglia, L. Serafini, "Model checking multiagent systems," Journal of Logic and Computation, vol. 8, no. 3, pp. 401-423, 1998. [online]. Available:

[12] D. J. T. Sumpter, G. B. Blanchard, "Ants and agents: a process algebra approach to modelling ant colony behaviour," Bulletin of Mathematical Biology, vol. 63, no. 5, pp. 951-980, 2001. [Online]. Available:

[13] A. Giua, C. Seatzu, "Modeling and supervisory control of railway networks using petri nets," Automation Science and Engineering, vol. 5, no. 3, pp. 431-445, 2008.

[14] G. Ali, S. Khan, N. A. Zafar, F. Ahmad, "Formal modeling towards a dynamic organization of multi-agent systems using communicating x-machine and z-notation," Indian Journal of Science and Technology, vol. 5, no. 7, pp. 2972-2977, 2012.

[15] S. Kouah, D. E. Saidouni, J. M. Ilie, "Synchronized petri net: A formal specification model for multi agent systems," Journal of Software, vol. 8, no. 3, pp. 587-602, 2013.

[16] S. Khosravifar, "Modeling multi agent communication activities with petri nets," International Journal of Information and Education Technology, vol. 3, no. 3, pp. 310-314, 2013. [online]. Available:

[17] L. Chang, X. He, S. M. Shatz, "A methodology for modeling multiagent systems using nested petri nets," International Journal of Software Engineering and Knowledge Engineering, vol. 22, no. 7, pp. 891-925, 2012. [Online]. Available:

[18] A. Pla, P. Gay, J. Melendez, B. Lopez, "Petri net-based process monitoring: A workflow management system for process modelling and monitoring," Journal of Intelligent Manufacturing, vol. 25, no. 3, pp. 539-554, 2014. [Online]. Available:

[19] A. David, L. Jacobsen, M. Jacobsen, K. Y. Jergensen, M. H. Meller, J. Srba, "Tools and Algorithms for the Construction and Analysis of Systems", pp. 492-497, Springer, 2012.

[20] T. A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, "Symbolic model checking for real-time systems," Information and computation, vol. 111, no. 2, pp. 193-244, 1994. [Online]. Available:

Awais QASIM, Syed Asad Raza KAZMI, Ilyas FAKHIR

Department of Computer Science, GC University, Lahore, Pakistan


Query                             Formula                 Result

Are all the stock markets         EF(!(STS.SM1 = 0) and   Satisfied
reachable?                        !(STS.SM 2 = 0) and
                                  !(STS.SM 3 = 0) and
                                  !(STS.SM4= 0))
Are both buying selling agents    EF(!(STS.BSA1 = 0) and  Satisfied
reachable?                        !(STS.BSA2 = 0))
Are both quoting agents           EF(!(STS.QA1 = 0) and   Satisfied
reachable?                        !(STS.QA2 = 0))
Is user agent reachable?          EF!(STSUA = 0)          Satisfied
Are SM1 Updates able to reach     EF STS.Goal_SM 1>=1     Satisfied
the UA within the deadline of 3
Are SM2 Updates able to reach     EF STS.Goal_SM 2 >= 1   Satisfied
the UA within the deadline of 5
Are SM3 Updates able to reach     EF STS.Goal_SM 3 >= 1   Satisfied
the UA within the deadline of 7
Are SM4 Updates able to reach     EF STS.Goal_SM 4 >= 1   Satisfied
the UA within the deadline of 8
TWA1 will never send an alert     AG STS.Goal_TWA1 = 0    Satisfied
older than 9 units to UA.
TWA2 will never send an alert     AG STS.Goal _TWA2 = 0   Satisfied
older than 9 units to UA.
BSA1 will never take more than    AG STS.Goal_BSA1 = 0    Satisfied
5 time units to buy/sell stocks.
BSA2 will never take more than    AG STS.Goal _BSA2 = 0   Satisfied
9 time units to buy/sell stocks.


Count  Transition          Max Tokens  Place

14     STS.T28             3           STS.CH1
10     STS.T17             2           STS.SM1
10     STS.T19             2           STS.SM2
10     STS.T21             2           STS.SM4
10     STS.T22             2           STS.BSA1
 9     STS.T18             2           STS.BSA2
 6     STS.T7              2           STS.UA
 4     STS.T6              1           STS.QA1
 3     STS.SM1_UPDATES     1           STS.QA2
 2     STS.T27             1           STS.SM3
 2     STS. [T.sub.3] 8    1           STS.TWA1
 1     STS.STOCK UPDATES1  1           STS.TWA2
 1     STS.STOCK_UPDATES2  1           STS.START
 1     STS.T23             1           STS.CH3
 1     STS.T24             1           STS.CH4
 1     STS.T26             1           STS.Goal SM1
 1     STS.T25             1           STS.Goal SM4
 1     STS.SM3 UPDATES     0           STS.CH2
 1     STS.SM4_UPDATES     0           STS.Goal_SM2
 1     STS. T35            0           STS.Goal_SM3
 1     STS. T36            unknown     STS.LU
 1     STS.T40
 0     STS.T29
 0     STS. T30
 0     STS. T32
 0     STS. T33
 0     STS. T37
 0     STS. T39
 0     STS.T41
COPYRIGHT 2015 Stefan cel Mare University of Suceava
No portion of this article can be reproduced without the express written permission from the copyright holder.
Copyright 2015 Gale, Cengage Learning. All rights reserved.

Article Details
Printer friendly Cite/link Email Feedback
Author:Qasim, Awais; Kazmi, Syed Asad Raza; Fakhir, Ilyas
Publication:Advances in Electrical and Computer Engineering
Date:Aug 1, 2015
Previous Article:Verification of Transformer Restricted Earth Fault Protection by using the Monte Carlo Method.
Next Article:An Analysis of a Hard Real-Time Execution Environment Extension for FreeRTOS.

Terms of use | Privacy policy | Copyright © 2021 Farlex, Inc. | Feedback | For webmasters |