Tomasz Rak

Jan Werewka

Performance Analysis of Interactive Internet Systems for a Class of Systems with Dynamically Changing Offers

This paper presents the performance analysis of interactive Internet systems, for which the time rate of system offer change is comparable to the users interaction time with the system. In this paper such systems class is called Interactive Internet Systems with Dynamically Changing Offers (IISDCO). In IISDCO systems an offer change may cause cancellation of the started but incomplete transactions. The necessity of cancellation can result from the sale of a set of resources (goods sold) which is getting exhausted or whose price has changed. This paper includes a performance analysis of an on-line stock exchange system (sample of IISDCO). For the analysis we used models in the form of Time Coloured Petri Nets (TCPNs). We also reviewed the proposed models on the example of the Internet on-line stock exchange system.

Introduction

In this paper we consider a certain class of interactive Internet systems. It is assumed that these systems perform maintenance bids quickly. Execution of transactions in these systems may be cancelled due to offer expiration. We will consider only the cases in which the number of transactions started within one second amounts to hundreds or thousands. We assume further, that a large part of the transaction will involve the same offer or the same range of products. In addition, the transaction process must take into account the results of a previous transaction connected with the same offer.

The presented system class is interesting from the practical point of view. A stock exchange system, with transactions carried out on-line, could be its representative. These transactions are performed in real time. Within each second, all over the world there are generated thousands of events related to the stock exchange. They must be sent in real time to participants, who can be located in various sites.

Today, many of the e-commerce systems are based on multi-layered and distributed structures [START_REF] Kounev | Performance Engineering of Distributed Component-Base Systems, Banchmarking, Modeling and Perrformance Prediction[END_REF]. The complexity of this architecture is difficult for the systems to provide the desired level of service (Quality of Service) [START_REF] Rak | The Modeling an Analysis of Interactive Internet Systems Realizing the Service of High-Frequency Offers[END_REF]. The major problems are as follows:

1) temporary heavy load, a large number of requests supported per second, 2) average response time increase, 3) resources overloading (system performance decrease).

On the other hand, developers are often faced with questions such as the following [START_REF] Kounev | Performance Modelling of Distributed E-Business Applications using Queuing Petri Nets[END_REF]:

1. How could performance change if load is increased? 2. What would the response time be? 3. Which components hale the largest effect on the overall system performance?

The remaining work is organized as follows. In Section 2, we introduce two-layered Internet distributed system. Section 3 presents performance analysis of TCPNs models. The last section sums up the paper and includes our future research plans.

Two-Layered Internet Distributed System

A typical architecture of the Internet is usually made up of several layers. The presented architecture (Fig. 1) is very popular on the Internet and is based on two layers: the frontend and back-end layer [START_REF] Pai | Locality-aware Request Distribution in Cluster-based Network Servers[END_REF]. The double-layer architecture was chosen because of the possibility of a full performance analysis of an Internet-based system.

The front-end layer (presentation-application) is based on the one hand on web servers and on application servers on the other. The presentation server is supposed to provide the customer with a system offer. The task of the application server is to manage the transactions. Modern application servers provide the cluster functionality, which allows the Load Balancing (LB). In case of any server failure, the request can be automatically forwarded to another node. The system architecture includes many servers to ensure greater efficiency of this layer. In case of complex systems, network services as LB [START_REF] Aversa | Load Balancing a Cluster of Web Servers Using Distributed Packet Rewriting[END_REF] or Domain Name Server are often used to distribute traffic. Software including these two functions in one layer (Tier 1 and 2) is for instance: Active Server Pages, Java Server Pages or PHP hypertext pre-processor.

The back-end layer (data) contains one or more databases (replication). This layer stores the systems data, and access to them is realized through transactions. Replication is applied:

1) when there are several different databases and data from them are replicated to a central database. 2) in order to speed up processing. It is profitable only if the database record processing is longer than the time needed to copy the processed records [START_REF] Rak | Database Replication in Practice[END_REF].

Performance Analysis

In this chapter we analyse performance metrics for the selected models of IISDCO architectures, such as the following layered models: basic (Model I), front-end cluster (Model II), front-end and back-end cluster (Model III) and front-end cluster and back-end cluster with replication (Model IV). The purpose of the models analysis is to demonstrate their suitability for modelling Web systems architectures. The analysis is based on TCPNs simulation studies. To present the system behaviour in various configurations, we present the selected simulation results, and adopt the following course of study. The characteristics of the arriving requests intensity with the same parameters are used for the simulation models [START_REF]Design/CPN homepage[END_REF] [10]. The process of requests arrival to the system is modelled by exponential distribution with the parameter, and throughput of service units by exponential distribution with µ parameter. The simulation is limited to three values for the exponential distribution. The main configuration of modeled system is determined by A -the number of nodes in the front-end layer and B -the number of nodes in the back-end layer:

TCPN Simulation Models

In our elaboration we created system models using TCPNs [START_REF] Rak | Distributed Internet Systems Modeling Using TCPNs[END_REF], which allow the performance analysis. We verified later the constructed models with the real experimental environment as a benchmark. During the simulation all queues were monitored, and in the first part of the research we examined their length.

Servers of the front-end layer are modelled by the use of the Processor Sharing (PS) queuing systems. PS1_A present a processing unit (PS1_A stands for an A-umpteenth queue system PS modelling a processing unit of the front-end layer). The back-end server presents the following queues: PS2_B modelling a processing unit, and FIFO2, cooperating with it and modelling a server disk (FIFO2_B stands for a B-umpteenth queue system FIFO modelling a storage data element in back-end layer).

Model I In case 1 the growing number of requests causes an increase of response waiting time. In the front-end and back-end layers we observe the increasing length of queues. Increasing the number of requests in the web-based system causes an increase in the response time as well. The client does not accept this time. For model I, in any case, unbalance is observed.

Case 1 (Fig. 2) with = 100 [1/s] illustrates a growth of PS1_1 queue. It leads to system unbalance, although the length of the back-end layers queues does not grow. Case 1 and = 300 [1/s] illustrates further increase of the PS1_1 queue. The effect is the same as in the previous case, i.e. the system unbalance. The lengths of the backend layer queues are on average about 1.5 for the PS2 and about 1.3 for FIFO2. There is some growth, but it is not critical for the balance of the system. Case 1 with = 500 [1/s] illustrates the front-end layer overload (by continuing to increase the length of PS1_1 queue to infinity). The effect is the same as in previous cases the whole system unbalance. This time, the lengths of the back-end layer queues are on average about 6.9 for PS2 and about 6 for FIFO2, and they keep growing. Cases for model II Analysis of the queues length (for a 2-and 4-node cluster installed in the front-end layer) in case of 100 [requests/s] would suggest that the problem is solved. However, in case of 300 [requests/s] the front-end queues are extended. The same happens with PS2 queue; its length increases almost ten times. For 500 [requests/s] the system balance is completely disturbed. Number of requests in the FIFO queue, especially in the case of 500 [requests/s], begins to grow alarmingly. A 4node cluster in the front-end layer copes somewhat better with the growing number of requests. In the case of 500 [requests/s] the response waiting time is extending. In the case of a front-end cluster layer model the system unbalance occurs for 500 [requests/s] both for the cluster A = 2 (Fig. 4a) and A = 4 (Fig. 4b). It results in an extension of all PS queues in both layers.

Characteristics for case 2 with

= 100 [1/s] indicate the system balance. The average queue length does not exceed the value of several pending requests. Figure 5 presents case 2 characteristics for = 300 [1/s], showing extension of the queue for this model. This is particularly evident in the case of PS2 queue length (Fig. 5c). However, it does not indicate the system unbalance. Increasing the load did not involve a loss of balance. The front-end layer characteristics (Fig. 5a,b) present a balance in the average length of almost several requests in the queue. The FIFO2 queue behaves similarly (Fig. 5d). Characteristics of case 2 with = 500 [1/s] illustrate loss of balance. All queues grow up to infinity. Only the value of the back-end layer FIFO queue is smaller. Another load increase results in a loss of balance.

Characteristics for case 3 with = 100 [1/s] illustrate the balanced system. Number of requests waiting in queues does not exceed 10 in this case. Characteristics for case 3 with = 300 [1/s], present unbalance in spite of increasing the number of servers in the front-end layer. The situation is similar to case 2 for A = 2. Increasing the number of cluster elements led to PS2 queue length shortening. Characteristics for case 3 with = 500 [1/s] present system unbalance. Reducing the queues length results in an improvement with relation to the same model for the case A = 2, but the unbalance remains. The graphs in (Fig. 6) present the response times of individual layers for model II with three different load values = 100 [1/s], 300 [1/s], 500 [1/s]. The graph in Fig. 6a presents a case when A = 2, while the graph in Fig. 6b presents a case when A = 4. We can observe the response time shortening with the largest load applied.

Cases for model III Another model to be analysed is model III (Fig. 7). We can see the performance improvement for the front-end cluster, but only in case when = 500 [1/s]. For case 4 the lengths of PS1_A queues grow along with the requests number increase. In case 5 PS1_A queues lengths are at a similar level for 100 and 300 [requests/s] and grow almost 100 times for 500 [requests/s]. In case 6 PS1_A queue lengths grow steadily several times for each of the three levels of load. This increase for 500 [requests/s] causes unbalance. Requests load of PS2_B queues for the case when B = 2 and for the case when B = 4 is maintained at the same level. They indicate the system unbalance. For the case when B = 4, the number of pending requests in the queues was about half as much. In FIFO2 queue the number of requests does not exceed 8 in any case. As a result of waiting for the requests realization in queues PS2_B the response time increases. Applying a similar number of nodes in the two layers makes the length of all queues shorten (in case of 4 nodes). In this instance the system unbalance is not as clear as for 100 [requests/s]. The system unbalance occurs in all other cases.

Characteristics of case 4 (Fig. 7a) with = 100 [1/s] show the system unbalance. Especially PS queues in the back-end layer present it. The same happens for case 4 with = 300 [1/s], 500 [1/s]. This time, PS queue of both system layers presents unbalance. A similar situation occurs in all model III cases (Fig. 7b).

Characteristics of case 6 (Fig. 7c) with = 100 [1/s] present the system unbalance. PS queue in the back-end layer presents unbalance, yet reduced almost ten times as compared to an identical model III with B = 2. Characteristics of case 6 with = 300 [1/s] present the system unbalance. PS queues in the back-end layer present unbalance. There can be observed the queues length reduction in comparison to an identical model III for B = 2. Characteristics of case 6 with = 500 [1/s] present the system unbalance, illustrated by PS queues in both layers, in another way as it was with the same model for the same parameters, except for B = 2. Concluding the analysis it seems advisable to use a similar number of nodes in both layers. Graphs in Fig. 8 present the response times for model III in particular layers with three different values of load. The graph in Fig. 8a presents case 4, the graph in Fig. 8b presents case 5, while the graph in Fig. 8c presents case 6. We can see extention of the response time in both layers, using the largest load. The response time of the front-end layer for the cases in (Fig. 8a,b) with = 500 [1/s] causes the system unbalance. With the largest load for the case in Fig. 8c increases. It presents a system unbalance. In cases 8 (Fig. 7b) and 9 (Fig. 7c) PS1_A queues lengths grow as well. However, in the case when A = 4 and B = 4, the number of requests waiting in the queue is not increasing that much. The number of requests in PS2_B queues remains on the level of both layers cluster model. For FIFO2_B queues the number of requests does not exceed 5 in any load case. The analysis of the requests number in the queues indicates the still inadequate level of requests service. In case 9 for 500 [requests/s] the growth is not that large, when compared to 300 [requests/s].

In model IV we can observe an opposite situation to that in previous cases. PS2_B queues are here the major reason for the system unbalance. Yet, despite the increasing load, the Internet system remains balanced as the number of nodes in the back-end layer grows. This behaviour is similar to model III. In this case we can observe reduction of number and equalization of the requests load in queues.

Characteristics of case 7 with = 100 [1/s] present the system unbalance (PS2_B queues). Characteristics of case 7 with = 300 [1/s], 500 [1/s] provide further system unbalancing (PS queues in two layers). A similar situation occurs in case 8 with = Graphs in (Fig. 11) present the response times of model IV particular layers with three different load values: = 100 [1/s], 300 [1/s], 500 [1/s]. The graph in Fig. 11a presents case 7, and the graph in Fig. 11b presents case 8, while the diagram in Fig. 11c presents case 9. There is a gradual shortening of the response time in layers for the largest peak load applied.

The presented detailed analysis of TCPN models illustrates trends that occur in cases when the system load is increasing. We should notice improvement in the system balance when using parallel processing (cluster). Distributing the requests among more nodes results in the improvement of system performance. On the other hand, using replication in the back-end layer does not cause such clear improvement, although it is a good solution, as can be observed particularly in case of increasing load. Graphs in figure 12 present a review of all behaviour patterns for particular loads. Model I has the longest response time that increases further on along with the load increase. The response times shape in the same way with declining tendency for models with clusters and replication (Fig. 12a,b,c).

Analysis Summary

Detailed conclusions from the IISDCO models analysis determine particular reactions to the load. Increasing the number of nodes in the front-end layer (using the cluster) results in accelerating the requests realization. For smaller loads such solution gives positive results. But the increase of requests number prolongs the response time. Using a cluster in the front-end and back-end layers results in shortening the response time in the front-end layer and lengthening it in the back-end layer. This disadvantageous state can be somewhat improved by enlarging the back-end layer cluster, yet the changes are not very significant. Only using a similar number of nodes in the back-end cluster/replication layer as in the front-end layer does provide a more satisfactory result in all cases. The use of replication implies the need for synchronization. The cost of synchronization is smaller than the profit obtained owing to additional service nodes. The load of each node is increased slightly, but on the whole the system reduces the response time by distributing the requests evenly. In cases where the unbalance is observed, there occurs e.g. a very short queue length of waiting requests in one layer and a very long one in another layer at the same time. The lack of balancing is associated with irregular distribution of loads in layers and between them.

The systems balance in the case of increasing load, is disturbed. Further increasing of the external load only worsens the performance. We could of course modify the hardware elements, yet this solution would mean greater costs and a necessity to exchange whole servers due to the devices incompatibility, for instance. We should rather concentrate on decentralised systems that are more natural for the Internet systems. It is assumed that to construct the systems identical computers were used. The effort was put into determining how they are connected. Basing on this analysis, it seems ap-propriate to apply the systems modification without interfering either in the computer construction or in software. In order to achieve systems balancing, it is necessary to: 1) use layers in the construction of systems, in order to balance the processed requests, 2) select the number of nodes in the cluster structured front-end layer, according to the actual load, 3) use replication with the number of nodes more than half the number of the front-end nodes.

Conclusion

The results obtained in models simulation, using TCPN and CSIM, were compared with experiments in Real On-line Internet Stock Exchange System (ROISES). ROISES is a simplified stock exchange Internet system constructed as a part of the IISDCO systems research. This software with appropriately selected parameters presents an example of IISDCO. In order to allow comparison of the developed models with the experiment results, a specific clients load stream was necessary to be used. The arrival stream was the same as the load used in the models. In addition, it was necessary to adjust the service time.

Experiments of the Internet stock reference model were limited to 4 nodes in the front-end layer and 2 nodes in the back-end layer due to the limited amount of equipment. The real system tests up to this moment are identical with the performance simulation models experiments in most cases. It was proved that the IISDCO performance models are correct. Despite the simplifications made in the models and on the assumptions given, an analysis reflecting the modelled reality can be provided. For layers response times the error remains within 15%. This is not a perfect model, but the error does not disqualify it in any way [START_REF] Menasce | Performance by Design[END_REF].

The advantages of this approach are:

1) verification of simulation models, 2) application of TCPN quantitative analysis, 3) using performance simulators, 4) the possibility of models expansion, 5) ability to monitor system elements during the simulation and experiments.

The obtained results are the basis for further study, concerning more complex processing models. Owing to the possibility of models further development, it will be possible to verify the system behaviour in case of a higher number of nodes and with greater input load. The preliminary results show that adequate modification of queuing systems parameters can produce acceptable level of compatibility between models and real systems.

Fig. 1 .

 1 Fig. 1. Internet system layers.

1 )

 1 case 1 model I (A = 1, B = 1), 2) case 2 model II (A = 2, B = 1); case 3 model II (A = 4, B = 1), 3) case 4 model III (A = 2, B = 2); case 5 model III (A = 4, B = 2); case 6 model III (A = 4, B = 4), 4) case 7 model IV (A = 2, B = 2); case 8 model IV (A = 4, B = 2); case 9 model IV (A = 4, B = 4). All systems have the same value on the exponential service parameter µ = 100 [1/s]. The study will encompass two performance parameters: queues length and response times in different layers. The final element of the performance analysis is a summary of the simulations results at the same simulation time, 100000 [s].

Fig. 2 .

 2 Fig. 2. Base model Model I for A = 1 and B = 1.

Figure 3

 3 Figure 3 presents the response times of individual layers of model I and three different types of load. Figure 3 illustrates this unbalance in the front-end layer.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Response time for model I case 1 -(front-end and back-end layer) with three load types.

Fig. 5 .

 5 Fig. 5. Sample queue length history for case 2 (300 [requests/s]): a) PS1 1, b) PS1 2, c) PS2, d) FIFO2.

Fig. 6 .

 6 Fig. 6. Response time for model II (front-end and back-end layer) with three load types: a) case 2, b) case 3.

Fig. 7 .

 7 Fig. 7. Model III and IV for (examples): a) cases 4 and 7, b) cases 5 and 8, c) cases 6 and 9.

Fig. 8 .Fig. 9 .

 89 Fig. 8. Response time for model III (front-end and back-end layer) with three load types: a) case 4, b) case 5, c) case 6.

Fig. 10 .

 10 Fig.10. Sample queue length history for case IV with 500[requests/s]: g) PS2 3, h) PS2 4, i) FIFO2 1, j) FIFO2 2, k) FIFO2 3, l) FIFO2 4.

Fig. 11 .

 11 Fig. 11. Response time for model IV (front-end and back-end layer) with three load types: a) case 7, b) case 8, c) case 9.

Fig. 12 .

 12 Fig. 12. Response time for all tested model cases (front-end and back-end layer) with three load types: a) 100[requests/s], b) 500[requests/s], c) 500[requests/s].


Bożena Woźna-Szcześniak

Bounded Model Checking for the Existential Part of Real-Time CTL and Knowledge

A considerably large class of multi-agent systems operate in distributed and real-time environments, and often their correctness specifications require us to express time-critical properties that depend on performed actions of the system. In the paper, we focus on the formal verification of such systems by means of the bounded model checking (BMC) method, where specifications are expressed in the existential fragment of the Real-Time Computation Tree Logic augmented to include standard epistemic operators.

Introduction

Model checking [START_REF] Clarke | Model Checking[END_REF] is an automatic and usually quite fast verification technique that can be applied to various hardware and software designs where specifications are given by formulae of modal logics. In model checking we represent a program as a labelled transition system (model), and describe a specification as a modal formula in order to check automatically whether the formula holds in the model.

In the last decade, the computer scientists have made tremendous progress in developing new model checking approaches. One of the most successful is called bounded model checking (see, among others, [START_REF] Penczek | Bounded Model Checking for the Universal Fragment of CTL[END_REF][START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF][START_REF] Sorea | Bounded Model Checking for Timed Automata[END_REF][START_REF] Woźna | Bounded Model Checking for the Universal Fragment of CTL*[END_REF][START_REF] Benedetti | Bounded Model Checking for Past LTL[END_REF][START_REF] Biere | Bounded Model Checking[END_REF][START_REF] Copty | Benefits of Bounded Model Checking at an Industrial Setting[END_REF]), and it has been introduced as a technique complementary to the BDD-based symbolic model checking method [START_REF] Bryant | Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification[END_REF]. The BMC method is an efficient SAT-based technique, especially designed for finding bugs in systems and producing counterexamples that can be used to point out the source of errors.

The main idea of BMC relies on looking for witnesses of an existential specification (or equivalently, searching for counterexamples of an universal specification) on suitable subsets of the full model of the system under consideration. Once a submodel is selected, the formula to be checked as well as the considered submodel are encoded as propositional formulae. Next, the propositional satisfiability of the conjunction of the two formulae mentioned above is solved by means of SAT solvers. If the satisfiability test is positive on the submodel, this means that the specification holds on the whole model; this is because an existential syntax is checked. If not, a larger submodel is selected and the whole procedure is run again.

The study of multi-agent systems (MAS) focuses on systems in which many intelligent agents (i.e., autonomous entities, such as software programs or robots) interact with each other. Their interactions can be either cooperative or selfish, that is, the agents can share a common goal or they can pursue their own interests. Also, each agent may have a deadline or other stated timing constraints to achieve an intended target. Reasoning about knowledge of such agents has always been a core concern in artificial intelligence, and thus many logical formalisms and verification techniques have been proposed and refined over the years, among others, [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Van Der Meyden | Symbolic Model Checking the Knowledge of the Dining Cryptographers[END_REF][START_REF] Fagin | What Can Machines Know? On the Properties of Knowledge in Distributed Systems[END_REF][START_REF] Raimondi | Automatic Verification of Multi-agent Systems by Model Checking via OBDDs[END_REF].

The aim of this paper is to develop a novel, SAT-based, verification techniques for logic-based specifications of the MAS, in which agents have time-limits or other explicit timing constraints to accomplish intended goals. In particular, we define a bounded model checking method in which a specification is expressed in the existential fragment of the Real-Time CTL augmented to include standard epistemic operators (RTECTLK). RTECTLK is an epistemic real-time computation tree logic that is the fusion [START_REF] Blackburn | Modal Logic[END_REF] of the two underlying languages: an existential fragment of real-time CTL (RTECTL) [START_REF] Emerson | Quantitative Temporal Reasoning[END_REF] and S5 n for the knowledge operators [START_REF] Fagin | Reasoning about Knowledge[END_REF]. RTECTL is a propositional branching-time temporal logic with bounded operators. It was introduced to permit specification and reasoning about distributed and real-time systems at the twin levels of abstraction: qualitative and quantitative. Obviously, defining the fusion with the full real-time CTL (RTCTL) would not be problematic, but we use here the fragment only because it is more suitable for the BMC method that is defined later on in the paper.

The bounded operators can be translated into nested applications of the EX operator, therefore the expressive power of the RTECTLK is the same as ECTLK [START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF]. However, this translation is often impractical, and RTECTLK provides a much more compact and convenient way of expressing time-critical (quantitative) properties.

To exemplify the use of the BMC techniques we also present a train controller system -a typical example of the multi-agent system.

The rest of the paper is organised as follows. In the next section the logic RTECTLK is introduced. Then, Section 3 defines the BMC method for RTECTLK. Section 4 shows how the BMC method can be applied to the train controller system. In Section 5 we conclude. The language RTECTLK is defined by the following grammar:

' := p | ¬p | ' ^' | ' _ ' | EX' | E('U I ') | | E('R I ') | K i ' | D ' | E ' | C ' . (1)
The remaining temporal operators are introduced in a standard way:

EF I ↵ def = E(trueU I ↵), EG I ↵ def = E(falseR I ↵)
. U I is the operator for bounded "Until", and the formula E(↵U I ) is read as "there exists a computation in which ↵ holds until, in the interval I, holds". R I is the operator for bounded "Release", and E(↵R I ) is read as "there exists a computation in which either holds until, in the interval I, both and ↵ hold, or always holds in the interval I". G I is the operator for bounded "Globally", and the formula EG I ↵ is read as "there exists a computation in which ↵ always holds in the interval I". F I is the operator for bounded "Eventually", and the formula EF I ↵ is read as "there exists a computation in which ↵ holds at some point in the interval I". K i is the operator dual for the standard epistemic modality K i , so K i ↵ is read as "agent i considers ↵ as possible". Similarly, the modalities D , E , C are the diamonds for D , E , C representing distributed knowledge in the group , "everyone in knows", and common knowledge among agents in .

Semantics. Traditionally, the semantics of temporal epistemic logics is given on interpreted systems [START_REF] Fagin | Reasoning about Knowledge[END_REF]. In this formalism each agent i 2 AG and the environment e are modelled by finite and non-empty sets of local states (L i and L e ), finite and non-empty sets of actions (Act i and Act e ), protocols (P i : L i ! 2 Acti and P e : L e ! 2 Acte ) and an evolution function

(t i : L i ⇥ L e ⇥ Act 1 ⇥ . . . Act n ⇥ Act e ! L i ).
Elements of L i capture the private information of agent i, and elements of L e capture the public information of environment e, which means that the other agents can have access to this information. Elements of Act i represent the possible actions that agent i is allowed to perform; for both the agents and the environment a special null action (denoted by ✏) is allowed, which corresponds to the agent or the environment performing no action. The protocol defines which actions may be performed in each local state of a given agent. Notice that the definition of protocols may enable more than one action to be performed for a given local state. When more than one action is enabled, it is assumed that an agent selects non-deterministically which action to perform. The evolution function defines how local states of a particular agent evolve based on the local states of the agent and the environment, and on actions of other agents. The environment e can be seen as a special agent that models the environment in which the agents operate; we refer to [START_REF] Fagin | Reasoning about Knowledge[END_REF] for more details on the above.

Let W = L 1 ⇥ • • • ⇥ L n ⇥ L e and Act = Act 1 ⇥ . . . Act n ⇥ Act e . Any element s 2 W is called a global state, and for a given global state s, l i (s) denotes the local state of agent i in s. Any element a 2 Act is called a joint action. A global evolution function t : W ⇥ Act ! W is defined as follows: t(s, a) = s 0 iff for all i 2 AG and e, t i (l i (s), a) = l i (s 0

) and t e (l e (s), a) = l e (s 0 ). Definition 1. For a given finite set of agents AG and a set of propositions PV, an interpreted system is a tuple IS = (hL i , Act i , P i , t i i i2AG , hL e , Act e , P e , t e i , ◆, V), where ◆ is an initial global state, and V : W ! 2 PV is an interpretation for the propositions in PV.

For a given interpreted system IS it is possible to associate a Kripke model M IS ; this model we will use to interpret the RTECTLK formulae. The model M IS = (S, T, {⇠ i } i2AG , ◆, V) is defined as follows:

-S ✓ W is a set of reachable global states; this is to avoid the epistemic accessibility of states that are not reachable from ◆ via the global evolution function t. -T ✓ S ⇥ S is a serial relation on S that is defined by the global evolution function t as follows: T(s, s 0 ) iff there exists an action a 2 Act such that t(s, a) = s 0 . -For each agent i 2 AG, ⇠ i ✓ S ⇥ S is an equivalence relation defined as follows:

s ⇠ i s 0 iff l i (s) = l i (s 0
).

-◆ is the initial global state of IS.

-The valuation function V : S ! 2 PV is the valuation function of IS that is restricted to the states from S only; the function assigns to each state a set of proposition variables that are assumed to be true at that state.

A path in M IS is an infinite sequence ⇡ = (s 0 , s 1 , . . .) of states such that (s i , s i+1 ) 2 T for each i 2 {0, 1, . . .}. For a path ⇡ = (s 0 , s 1 , . . .), we take ⇡(i) = s i . By ⇧(s) we denote the set of all the paths starting at s 2 S. Moreover, for the group epistemic modalities we also define the following. If ✓ AG, then

⇠ E def = S i2 ⇠ i , ⇠ C def = (⇠ E ) + (
IS , s |= p iff p 2 V(s), M IS , s |= ↵ _ iff M IS , s |= ↵ or M IS , s |= , M IS , s |= ¬p iff p 6 2 V(s), M IS , s |= ↵ ^ iff M IS , s |= ↵ and M IS , s |= , M IS , s |= EX↵ iff 9 ⇡ 2 ⇧(s) such that M IS , ⇡(1) |= ↵, M IS , s |= E(↵U I ) iff (9 ⇡ 2 ⇧(s))(9 m 2 I) [M IS , ⇡(m) |= and (8 j < m) M IS , ⇡(j) |= ↵], M IS , s |= E(↵R I ) iff 9 ⇡ 2 ⇧(s) such that either (8 m 2 I) M IS , ⇡(m) |= or (9 m 2 I) [M IS , ⇡(m) |= ↵ and (8 j  m) M IS , ⇡(j) |= ], M IS , s |= K i ↵ iff (9 s 0 2 S)(s ⇠ i s 0 and M IS , s 0 |= ↵), M IS , s |= D ↵ iff (9 s 0 2 S)(s ⇠ D s 0 and M IS , s 0 |= ↵), M IS , s |= E ↵ iff (9 s 0 2 S)(s ⇠ E s 0 and M IS , s 0 |= ↵), M IS , s |= C ↵ iff (9 s 0 2 S)(s ⇠ C s 0 and M IS , s 0 |= ↵). Definition 3. A RTECTLK formula ' is valid in M IS (denoted M IS |= ') iff M IS , ◆ |= ', i.e.,
' is true at the initial state of the model M IS .

Bounded Model Checking

Like any other BMC method, also the one defined in this section consists in translating the model checking problem for the RTECTLK into the problem of satisfiability of a propositional formula. In this translation the solution for the epistemic part of the RTECTLK follows the one presented in [START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF].

We start by defining a notion of k-bounded semantics for the RTECTLK, where k 2 N + = {1, 2, . . .}. Then, we prove that the model checking problem for a RTECTLK formula can be reduced to the bounded model checking problem for this formula. Finally, we show that the model checking problem for the RTECTLK can be reduced to the satisfiability problem of a propositional formula that is a conjunction of two formulae: the first one encodes a fragment of a model under consideration unfolded up to the depth k, and the second one encodes the checked RTECTLK formula.

Bounded Semantics of RTECTLK

We begin with some auxiliary definitions. Let M IS be a model associated to an interpreted system IS, and

k 2 N + a bound. A k-path ⇡ in M IS is a finite sequence of states (s 0 , . . . , s k ) such that (s i , s i+1 ) 2 T for each 0  i < k. A k-path ⇡ = (s 0 , . . . , s k
) is an a-loop for some a 0, if there exists a  l  k such that T(⇡(k), ⇡(l)). By ⇧ k (s) we denote the set of all the k-paths starting at s in M IS . Note that this set is a convenient way of representing the k-bounded subtree rooted at s of the tree resulting from unwinding the model M IS from s. Moreover, if a k-path is an a-loop, then it represents an infinite path.

In the bounded case satisfaction of the temporal operator ER I with I = [b, 1) or I = (b, 1) on a k-path ⇡ depends on whether or not ⇡ is an a-loop. Therefore, we introduce a function loop : ⇧ k ⇥ N ! 2 N that allows for the identification of the kpaths that are actually a-loops. This function is defined by: loop

(⇡, a) = {l | a  l  k and T(⇡(k), ⇡(l))} for some a 0. Further, if I is an interval of the form [a, b], [a, b), (a, b], (a, b), [a, 1
) and (a, 1), then by left(I) we denote the left end of the interval I, i.e., left(I) = a. Definition 4. Let M IS be a model associated to an interpreted system IS, and k

2 N + a bound. A k-model for M IS is a structure M k = (S, P k , {⇠ i } i2AG , ◆, V), where P k = S s2S ⇧ k (s).
Now we can define a notion of bounded satisfaction for the RTECTLK formulae on bounded structures. Definition 5. Let k 2 N + , M IS be a model associate to an interpreted system IS, M k its k-model, and ↵, RTECTLK formulae. M k , s |= ↵ denotes that ↵ is true at the state s of M k . The satisfaction relation |= is defined inductively as follows:

M k , s |= p iff p 2 V(s), M k , s |= ↵ _ iff M k , s |= ↵ or M k , s |= , M k , s |= ¬p iff p 6 2 V(s), M k , s |= ↵ ^ iff M k , s |= ↵ and M k , s |= , M k , s |= EX↵ iff (9 ⇡ 2 ⇧ k (s))M k , ⇡(1) |= ↵, M k , s |= E(↵U I ) iff (9 ⇡ 2 ⇧ k (s))(9 0  j  k)(j 2 I and M k , ⇡(j) |= and (8 0  i < j) M k , ⇡(i) |= ↵), M k , s |= E(↵R I ) iff (9 ⇡ 2 ⇧ k (s))(9 0  j  k)[(j 2 I and M k , ⇡(j) |= ↵ and (8 0  i  j)M k , ⇡(i) |= ) or (8 j 2 I)(M k , ⇡(j) |= and I \ [0, k] = I) or (8 left(I) < j  k)(M k , ⇡(j) |= and loop(⇡, left(I) + 1) 6 = ;) or (8 left(I)  j  k) (M k , ⇡(j) |= and loop(⇡, left(I)) 6 = ;)], M k , s |= K i ↵ iff (9 ⇡ 2 ⇧ k (◆))(9 0  j  k)(M k , ⇡(j) |= ↵ and s ⇠ i ⇡(j)), M k , s |= D ↵ iff (9 ⇡ 2 ⇧ k (◆))(9 0  j  k)(M k , ⇡(j) |= ↵ and s ⇠ D ⇡(j)), M k , s |= E ↵ iff (9 ⇡ 2 ⇧ k (◆))(9 0  j  k)(M k , ⇡(j) |= ↵ and s ⇠ E ⇡(j)), M k , s |= C ↵ iff (9 ⇡ 2 ⇧ k (◆))(9 0  j  k)(M k , ⇡(j) |= ↵ and s ⇠ C ⇡(j)). A RTECTLK formula ' is valid in k-model M k (denoted M |= k ') iff M k , ◆ |= ', i.e., ' is true at the initial state of the k-model M k .

Equivalence of Bounded and Unbounded Semantics

We start with some auxiliary definitions. By straightforward induction on the length of a RTECTLK formula ' we can show that the following lemma holds.

Lemma 1. Let k 2 N + , M IS be a model associated to an interpreted system IS, M k its k-model, and ' a RTECTLK formula. Then, for any s in M IS , M k , s |= ' implies M IS , s |= '.

Lemma 2. Let M IS be a model associated to an interpreted system IS, M k its k-model, ' a RTECTLK formula, s a state of M IS , and k = bmax{Max(BI(')), Max(UI('

))}/ | M IS |c⇤ | M IS | + | M IS |. If M IS , s |= ', then M k , s |= '.
Proof (By induction on the length of '). The lemma follows directly for the propositional variables and their negations. Next, assume that the hypothesis holds for all the proper sub-formulae of '. If ' is equal to either ↵ ^ , ↵ _ , or EX↵, then it is easy to check that the lemma holds. For the epistemic operators, i.e., ' = K l ↵, E ↵, D ↵, C ↵, the proof is like in [START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF] (see Lemma 2). So, consider ' to be of the following forms: -Assume that (1) holds and I = (b, 1) for some b 0. The proof is analogous to the case above. Assume that (2) holds. The proof is analogous to the until case.

The main theorem of this section states that bmax{Max(BI(')), Max(UI(' Proof. The proof follows from Lemmas 1 and 2.

))} / | M IS |c⇤ | M IS | + | M IS |-

Submodels of k-models

The previous subsection ends with the conclusion that to check whether a model M IS associated to an interpreted system IS is a model to a RTECTLK formula ' under consideration, it is enough to check whether ' holds on the k-model M k , for some

k  bmax{Max(BI(')), Max(UI('))}/ | M IS |c⇤ | M IS | + | M IS |.
In this subsection we prove that ' holds on M IS if and only if ' holds on a submodel of M k .

Definition 6. A submodel of a k-model M k = (S, P k , {⇠ i } i2AG , ◆, V) is a tuple M 0 (s) = (S 0 , P 0 k , {⇠ 0 i } i2AG , s, V 0 ) rooted at state s 2 S such that P 0 k ✓ P k , S 0 = {r 2 S | (9 ⇡ 2 P 0 k )(9 i  k)⇡(i) = r} [ {s}, ⇠ 0 i =⇠ i \(S 0 ⇥ S 0
) for each i 2 AG, and V 0 = V ⌫ S 0 . Satisfaction for RTECTLK over a submodel M 0 (s) is defined as for M k . Now, we introduce a function f k that gives a bound on the number of k-paths in the submodel M 0 (s). Namely, the function f k : RTECTLK ! N is defined by:

f k (p) = f k (¬p) = 0, where p 2 PV 0 , f k (↵ _ ) = max{f k (↵), f k ( )}, f k (E(↵U I )) = k•f k (↵)+ f k ( ) + 1, f k (Y↵) = f k (↵) + 1, for Y 2 {K i , D , E }, f k (↵ ^ ) = f k (↵) + f k ( ), f k (E(↵R I )) = (k + 1) • f k ( ) + f k (↵) + 1, f k (C ↵) = f k (↵) + k.
In the following, we will show that the validity of ' in M k is equivalent to the validity of ' in M 0 (s) provided that the bound k is chosen by means of the function f k . We start with an auxiliary Lemma 3 that can be proved by straightforward induction on the length of a RTECTLK formula '. Lemma 3. Let M 0 (s) and M 00 (s) be two submodels of M k with P 0 k ✓ P 00 k , and '

a RTECTLK formula. If M 0 (s) |= k ', then M 00 (s) |= k '. Lemma 4. M k , s |= ' iff there is a submodel M 0 (s) of M k with | P 0 k | f k (') such that M 0 (s), s |= '. Proof.
The implication from right to left is straightforward. To prove the implication left to right, we will use induction on the length of '.

The "left-to-right" implication follows directly for the propositional variables and their negations. Next, assume that the hypothesis holds for all the proper sub-formulae of '. If ' = ↵ ^ or ' = ↵ _ , then the proof is straightforward. For the epistemic operators, i.e., ' = K l ↵, E ↵, D ↵, C ↵, the proof is like in [START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF] (see Lemma 3). For ' = EX↵ the proof is like in [START_REF] Penczek | Bounded Model Checking for the Universal Fragment of CTL[END_REF] (see Lemma 3). Consider ' to be of the following forms:

• Let ' = E(↵U I ) and M k , s |= '. By the definition, there is a k-path ⇡ 2 ⇧ k (s) such that (9 m 2 I)(M k , ⇡(m) |= and (8 0  i < m)M k , ⇡(i) |= ↵). Hence, by the inductive assumption, (1) for all i such that 0  i < m there are submodels

M i (⇡(i)) of M k with | P i k | f k (↵) and M i (⇡(i)), ⇡(i) |= ↵, (2) and there is a sub- model M m (⇡(m)) of M k with | P m k | f k ( ) and M m (⇡(m)), ⇡(m) |= . Consider a submodel M 0 (s) of M k such that P 0 k = S m i=0 P i k [ {⇡}.
Thus, by the construction of M 0 (s), we have that ⇡ 2 P 0 k . Therefore, since conditions (1), and (2) hold, by the definition of the bounded satisfaction, we have that M 0 (s), s |= E(↵U I ) and

| P 0 k | k • f k (↵) + f k ( ) + 1. • Let ' = E(↵R I ) and M k , s |= '. By the definition of bounded semantics, there is a k-path ⇡ 2 ⇧ k (s) such that (9 j 2 I)(M k , ⇡(j) |= ↵ and (8 0  i  j)M k , ⇡(i) |= ) or (2)
(8 j 2 I)(M k , ⇡(j) |= and I \ [0, k] = I) or (3)
(8 left(I) < j  k)(M k , ⇡ (
Let us consider the four cases. First, assume that condition (2) holds. Then, by the inductive assumption, for all i such that 0  i  j there are submodels

M i (⇡(i)) of M k with | P i k | f k ( ) and M i (⇡(i)), ⇡(i) |= , (6)
and there is a submodel

M 00 (⇡(m)) of M k with | P 00 k | f k (↵) and M 00 (⇡(m)), ⇡(m) |= ↵ . ( 7
)
Consider the submodel M 0 (s) of M k such that P 0 k = S j i=0 P i k [ P 00 k [ {⇡}. Thus, by the construction of M 0 (s), we have that ⇡ 2 P 0 k . Therefore, since the conditions (2), ( 6) and ( 7) hold, by the definition of the bounded satisfaction we have that M 0 (s), s |= E(↵R I ) and

| P 0 k | (k + 1) • f k ( ) + f k (↵) + 1.
Assume now that condition (3) holds. Then, by the inductive assumption, for all j such that j 2 I there are submodels M j (⇡(j)) of M k with | P j k | f k ( ) and

(M j (⇡(j)), ⇡(j) |= ) . (8)
Consider the submodel M 0 (s) of M k such that P 0 k = S j2I P j k [ {⇡}. Thus, by the construction of M 0 (s), we have that ⇡ 2 P 0 k . Therefore, since conditions ( 2) and ( 8) hold, by the definition of bounded satisfaction we have that M 0 (s), s |= E(↵R I ) and

| P 0 k | (k + 1) • f k ( ) + f k (↵) + 1.
The remaining two cases can be proved similarly.

The following theorem shows that a RTECTLK formula ' holds on M IS if and only if ' holds on a submodel M 0 (◆) of M k . Theorem 2. Let M IS be a model associated to an interpreted system, M k its k-model, ' a RTECTLK formula, and k = bmax{Max(BI(')), Max(UI('

))}/ | M IS |c⇤ | M IS | + | M IS |. Then, M IS |= ' iff there exists a submodel M 0 (◆) of M k with P 0 k  f k (') and M 0 (◆) |= k '.
Proof. Follows from Theorem 1 and Lemma 4.

Translation to Boolean Formulae

Given a RTECTLK formula ' and a model M IS . As it was already mentioned, the main idea of the BMC method for the RTECTLK consists in translating the model checking problem for the RTECTLK into the satisfiability problem of a propositional formula

[M IS , '] k that is a conjunction of two formulae, i.e.: [M IS , '] k = [M ',◆ IS ] k ^['] Mk . [M ',◆
IS ] k represents all the possible submodels of M IS that consist of f k (') k-paths of M IS , and

['] Mk encodes constraints that must be satisfied by f k (')-submodels of M IS for ' to be satisfied. Once this translation is defined, checking satisfiability of a resulting formula can be done by means of a SAT-checker.

In order to define the formula [M IS , '] k we proceed as follows. We assume that each state s of M IS is encoded by a bit-vector whose length, say n, depends on the number of agents' local states. Thus, each state s of M IS we can represent by a vector w = (w[1], . . . , w[n]) of propositional variables (usually called state variables) to which we refer to as a global state variable. A finite sequence (w 0 , . . . , w k ) of global state variables we call a symbolic k-path. Since, in general, we may need to consider more than one symbolic k-paths, we introduce a notion of the j-th symbolic k-path, which is denoted by (w 0,j , . . . , w k,j ), where w i,j are global state variables for 1  j  f k (') and 0  i  k. Note that the exact number of necessary symbolic k-paths depends on the checked formula ', and it can be calculated by means of the function f k .

For two global state variables w, w 0 , we define the following propositional formulae:

• I s (w) is a formula over w that is true for a valuation s w of w iff s w = s.

• p(w) is a formula over w that is true for a valuation s w of w iff p 2 V(s w ) (encodes a set of states of M IS in which p 2 PV holds). • H(w, w 0

) is a formula over w and w 0 that is true for two valuations s w of w and s w 0 of w 0 iff s w = s w 0 (encodes equivalence of two global states).

• H i (w, w 0

) is a formula over w, w 0 that is true for two valuations s w of w and s w 0 of w 0 iff l i (s w ) = l i (s w 0

) (encodes equivalence of local states of agent i). • R(w, w 0

) is a formula over w, w 0 that is true for two valuations s w of w and s w 0 of w 0 iff (s w , s w 0 ) 2 T (encodes the transition relation of M IS ). Let a, b be vectors of propositional formulae built only over propositional constants true and false; note that the vectors a and b can be seen as bit-vectors. We define the following auxiliary propositional formulae:

• ⇥ : {0, . . . , 2 t
1} ! {true, false} t is a function that converts each natural number smaller than 2 t to the bit-vector of the length t.

• eq(a, b) := V t i=1 a[i] , b[i], ge(a, b) := W t i=1 a[i] ^¬b[i] ^Vt j=i+1 a[j] , b[j] , geq(a, b) := eq(a, b) _ ge(a, b), le(a, b) := ¬geq(a, b), leq(a, b) := ¬ge(a, b), • IN(j, I) := 8 > > > > > > < > > > > > > : le(⇥(a), ⇥(j)) ^le(⇥(j), ⇥(b)), if I = (a, b) leq(⇥(a), ⇥(j)) ^leq(⇥(j), ⇥(b)), if I = [a, b] leq(⇥(a), ⇥(j)) ^le(⇥(j), ⇥(b)), if I = [a, b) le(⇥(a), ⇥(j)) ^leq(⇥(j), ⇥(b)), if I = (a, b] ge(⇥(a), ⇥(j)), if I = (a, 1) geq(⇥(a), ⇥(j)), if I = [a, 1)
The formula IN(j, I) encodes that j 2 I.

A. Let ' = E(↵U I ) and M 0 k , s |= ' with | P 0 k | f k (')
. By the definition of the bounded semantics we have that there is a k-path ⇡ 2 ⇧ k (s) and exists 0  j  k such that j 2 I and M 0 k , ⇡(j) |= and M 0 k , ⇡(t) |= ↵ for all 0  t < j. Hence, by induction we obtain that for some j  k and j 2 I the propositional formula IN(j, I) is satisfiable, and also the following propositional formula are satisfiable:

[ ] [0,0] k ^[M ,⇡(j)
] k and [↵]

[0,0] k ^[M ↵,⇡(t)
] k , for each t  j. Let i be the index of a new symbolic k-path which satisfies the formula H(w 0,0 , w 0,i ). Because of the above and Lemma 3, we obtain that the propositional formula H(w 0,0 , w 0,i ) Ŵk

j=0 [ ] [j,i] k ^IN(j, I) ^Vj 1 t=0 [↵] [t,i] k ^[M E(↵UI ),⇡(0)
] k is satisfiable. Therefore, the following propositional formula is satisfiable too:

W f (') i=1 H(w m,n , w 0,i ) Ŵk j=0 ([ ] [j,i] k ^IN(j, I) ^Vj 1 t=0 [↵] [t,i] k ) ^[M E(↵U ),⇡ (0)
] k . Hence, by the definition of the translation of a RTECTLK formula, the above formula is equal to the propositional formula [E(↵U I )]

[0,0] k ^[M E(↵UI ),⇡(0)
] k . B. Let ' = E(↵R I ). The formal proof of the case is tedious and can be done in a similar way as the one for the EU I operator. So, we have decided not to present it in detail.

Theorem 3. Let M IS be a model, and ' a RTECTLK formula. Then, M IS |= ' iff there

exists k > 0 such that ['] Mk ^[M ',◆
] k is satisfiable. Proof. It follows from Theorem 2 and Lemma 5.

A Train Controller System

We now give an example of how the RTECTLK formalism can be used to reason about MASs and, in particular, how the RTECTLK properties of a MAS can be verified using the BMC technique described in the paper. The system we consider is a train controller (TC), adapted from [START_REF] Van Der Hoek | Cooperation, Knowledge, and Time: Alternating-time Temporal Epistemic Logic and its Applications[END_REF], and it consists of two trains and a controller. In the system it is assumed that each train uses its own circular track (the Eastbound or the Westbound) for travelling in one direction. At one point, both trains have to pass through a tunnel, but because there is only one track in the tunnel, trains arriving from each direction cannot use it simultaneously. There are traffic lights on both sides of the tunnel, which can be either red or green. The controller is notified by both trains when they request entry to the tunnel or when they leave the tunnel, and controls the colour of the traffic lights.

In the interpreted systems framework, the TC system can be modelled by three agents: two trains (agents 1 and 3) and a controller (agent 2). Their local states are the following: L 1 = {away 1 , wait 1 , tunnel 1 }, L 2 = {green, red}, L 3 = {away 2 , wait 2 , tunnel 2 }. The state away i represents the initial state of train i. The state wait i represents that train i has arrived at the tunnel. The state tunnel i represents that train i is in the tunnel. The states green and red represent the colour of the traffic lights.

Given the sets of local states for the above tree agents, the following sets of actions are available to the agents: Act 1 = {a 1 , a 2 , a 3 , ✏}, Act 2 = {a 2 , a 3 , a 5 , a 6 , ✏}, Act 3 = {a 4 , a 5 , a 6 , ✏}. Their meaning is the following: a 1 (a 4 ) -train 1 (train 2) has arrived at the tunnel; a 2 (a 5 ) -colour of the traffic lights for train 1 (train 2) is green; a 3 (a 6 ) -train 1 (train 2) has left the tunnel. The protocols executed by agents are defined by: P 1 (away 1 ) = {a 1 }, P 1 (wait 1 ) = {a 2 }, P 1 (tunnel 1 ) = {a 3 }, P 3 (away 2 ) = {a 4 }, P 3 (wait 2 ) = {a 5 }, P 3 (tunnel 2 ) = {a 6 }, P 2 (green) = {a 2 , a 5 }, P 2 (red) = {a 3 , a 6 }. The evolution of the TC system is defined by means of an evolution function t

: (L 1 ⇥ L 2 ⇥ L 3 ) ⇥ Act ! (L 1 ⇥ L 2 ⇥ L 3 ), where Act is a subset of Act 1 ⇥ Act 2 ⇥ Act 3 .
More precisely, let us assume that the TC system starts from the following initial state:

(away 1 , green, away 2 ), and let green = g, red = r, tunnel i = t i , away i = aw i , wait i = w i , for i = 1, 2. Then, the evolution function for the TC system is defined as follows: t((aw 1 , g, aw 2 ), (a 1 , ✏, ✏)) = (w 1 , g, aw 2 ), t((aw 1 , g, aw 2 ), (✏, ✏, a 4 )) = (aw 1 , g, w 2 ), t((w 1 , g, aw 2 ), (a 2 , a 2 , ✏)) = (t 1 , r, aw 2 ), t((w 1 , g, aw 2 ), (✏, ✏, a 4 )) = (w 1 , g, w 2 ), t((aw 1 , g, w 2 ), (a 1 , ✏, ✏)) = (w 1 , g, w 2 ), t((aw 1 , g, w 2 ), (✏, a 5 , a 5 )) = (aw 1 , r, t 2 ), t((t 1 , r, aw 2 ), (✏, ✏, a 4 )) = (t 1 , r, w 2 ), t((t 1 , r, aw 2 ), (a 3 , a 3 , ✏)) = (aw 1 , g, aw 2 ), t((w 1 , g, w 2 ), (a 2 , a 2 , ✏)) = (t 1 , r, w 2 ), t((w 1 , g, w 2 ), (✏, a 5 , a 5 )) = (w 1 , r, t 2 ), t((aw 1 , r, t 2 ), (a 1 , ✏, ✏)) = (w 1 , r, t 2 ), t((aw 1 , r, t 2 ), (✏, a 6 , a 6 )) = (aw 1 , g, aw 2 ), t((t 1 , r, w 2 ), (a 3 , a 3 , ✏)) = (aw 1 , g, w 2 ), t((w 1 , r, t 2 ), (✏, a 6 a 6 )) = (w 1 , g, aw 2 ). It determines not only the set of reachable global states S ✓ L 1 ⇥ L 2 ⇥ L 3 , but also gives the transition relation T; namely, for all the s, s 0 2 S, (s, s 0 ) 2 T iff there exists act 2 Act such that t(s, act) = s 0 .

We have now defined reachable states, actions, protocols, and transitions of the model M IS = (S, T, {⇠ i } i2AG , ◆, V) for the TC system. Let PV = {inW 1 , inW 2 , inT 1 , inT 2 } be a set of propositional variables, which we find useful in analysis of the scenario of the TC system. To conclude, we define a valuation function V : S ! 2 PV as follows:

inT 1 2 V(s) if l 1 (s) = tunnel 1 , inT 2 2 V(s) if l 2 (s) = tunnel 2 , inW 1 2 V(s) if l 1 (s) = wait 1 , and inW 2 2 V(s) if l 2 (s) = wait 2 .
We have now completed the definition of the model M IS for the TC system, so we can proceed to the verification of the model M IS by means of the BMC method. As an example, let us verify the following properties:

-There exists a behaviour of the TC system such that agent Train i (for i = 1 or i = 3) considers possible a situation in which it is not true that being in the tunnel always leads to the same situation within a bounded period of time, i.e., within n time units for n 2. This property can be formalised by the following RTECTLK formula:

↵ := EF [0,1] K i (inT i ^EG [0,n] (¬inT i )).
-There exists a behaviour of the TC system such that agent Train i (for i = 1 or i = 3) considers possible a situation in which both he is in his waiting state and in the next state he still waits for the permission to enter the tunnel. This property can be formalised by the following RTECTLK formula:

:= EF [0,1] K i (inW i ÊX(¬inT i )).
-The model of the TC system does not satisfy the property of n-bounded fairness, i.e., each train should be scheduled for entering the tunnel at least once every n steps of the system, for n 3. This property can be formalised by the following RTECTLK formula:

:= EG [0,n] (¬inT 1 ) _ EG [0,n] (¬inT 2 ) _ EF [0,1] (¬inT 1 ÊXEG [0,n 1] (¬inT 1 )) _ EF [0,1] (¬inT 2 ^EXEG [0,n 1] (¬inT 2 )).
According to the BMC algorithm for the RTECTLK, to perform the method for the TC system and properties ↵, , and , first, all the states of M IS have to be represented by bit-vectors. To do this we have to encode all the possible configurations of the system in terms of local states of agents. So, assume that we have the following bit representation of local states. For Train 1 we take away 1 = (0, 0), wait 1 = (0, 1), tunnel 1 = (1, 0), for Train 2 away 2 = (0, 0), wait 2 = (0, 1), tunnel 2 = (1, 0), and for Controller green = (0) and red = (1). So, the global states of the TC system have the following encoding: (away 1 , green, away 2 ) = (0, 0; 0; 0, 0), (wait 1 , green, away 2 ) = (0, 1; 0; 0, 0), (tunnel 1 , red, away 2 ) = (1, 0; 1; 0, 0), etc. In other words, we need 5 state variables (s[0], . . . , s [START_REF] Bryant | Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification[END_REF]) to encode all the possible configurations of the TC system. Next, the transition relation of M IS has to be encoded by a propositional formula, and formulae ↵, and have to be translated over all the possible f k (↵) = 3 (resp. f k ( ) = 3, f k ( ) = 3) submodels of M IS .

To proceed with the translation of the transition relation of M IS , the first thing we need to translate is the initial state ◆ = (away 1 , green, away 2 ) of the TC system that is represented by the bit-vector (0, 0, 0, 0, 0). With this representation ◆ will be encoded by the following propositional formula I ◆ (w 0,0 ) = V 4 i=0 (¬ w 0,0 [i]). The next step is to translate the transitions R(w i,j , w i+1,j ), for i = 0, .., k 1 and j = 1, 2, 3. For simplicity we report only on the formula R(w 0,1 , w 1,1 ) representing the first transition of the first path. Let us consider the following transition of our counterexample: T((away 1 , green, away 2 ), (wait 1 , green, away 2 )). The corresponding formula is: R(w 0,1 , w 1,1 ) :=

In order to encode the whole example we should model all the transitions for all the k's starting from k := 1. We do not do it here.

To encode the translation of ↵, and , first we need to encode the propositions used in these formulae. Namely, inT 1 (w) := (w[0] ^¬w [START_REF] Benedetti | Bounded Model Checking for Past LTL[END_REF]), which means that inT 1 holds at all the global states with the first local state equal to (1, 0). inT 2 (w) := (w [START_REF] Blackburn | Modal Logic[END_REF] ^¬w [START_REF] Bryant | Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification[END_REF]), which means that inT 2 holds at all the global states with the third local state equal to (1, 0). inW 1 (w) := (¬w[0] ^w [START_REF] Benedetti | Bounded Model Checking for Past LTL[END_REF]), which means that inW 1 holds at all the global states with the first local state equal to (0, 1). inW 2 (w) := (¬w [START_REF] Blackburn | Modal Logic[END_REF] ^w [START_REF] Bryant | Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification[END_REF]), which means that inW 2 holds at all the global states with the third local state equal to (0, 1).

In so doing, it is sufficient to unfold the formula [↵] Checking that the TC system satisfies the RTECTLK formulae above can now be done by feeding a SAT solver with the propositional formula generated by this method. This would produce a solution, thereby proving that the constructed propositional formula is satisfiable.

Conclusions

In summary, we have shown how to extend the BMC method to the RTECTLK formalism, and we have proved that the RTECTLK bounded model checking can be solved in time O(bmax{Max(BI(')), Max(UI('))}/ | M IS |c⇤ | M IS | + | M IS |). We have also considered a train controller system to exemplify a use of the proposed method.

The underlying semantics of time of the considered MASs and the RTECTLK formalism is discrete. However, it is also possible to consider real-time multi-agent systems under the assumption that the time is dense and properties are express in TCTLK; such an attempt has been done in [START_REF] Woźna | Bounded Model Checking for Knowledge over Real Time[END_REF].

Finally we should like to stress that this paper belongs to a line of research on model checking time and knowledge encompassing theoretical investigations. A comparison of the experimental results with other model checking technique for MASs we leave for further work.

2

  The Logic RTECTLK Syntax. Let PV be a set of propositional variables, p 2 PV, AG a finite set of agents, i 2 AG, ✓ AG, and I an interval in N = {0, 1, 2, . . .} of the form: [a, b], [a, b), (a, b], (a, b), (a, 1), and [a, 1), for a, b 2 N.

  By | M IS | we denote the size of M IS , i.e., the sum of the elements of the set S and the elements of the set T. If I is an interval of the form [a, b], [a, b), (a, b], (a, b), [a, 1) and (a, 1), for a, b 2 N, then by right(I) we denote the right end of the interval I, i.e., right(I) = b if b 2 N, and otherwise right(I) = 1. Further, let ' be a RTECTLK formula. Then, we denote by BI(') the set of all the bounded intervals (i.e., intervals of the form [a, b], [a, b), (a, b], (a, b)) that appear in ', by UI(') the set of all the unbounded intervals (i.e., intervals of the form [a, 1), (a, 1)) that appear in ', by Max(BI(')) the maximal value of the set {b | right(I) = b and I 2 BI(')}, and by Max(UI(')) the maximal value of the set {a | left(I) = a and I 2 UI(')}.

1 .

 1 Let ' = E(↵U I ). From the unbounded semantics we have that there exist a path ⇡ 2 ⇧(s) and m 2 I such that M IS , ⇡(m) |= and M IS , ⇡(i) |= ↵ for all 0  i < m. Since m 2 I and k = bmax{Max(BI(')), Max(UI('))}/ | M IS |c⇤ | M IS | + | M IS |, then it is easy to see that m  k. Thus, by the inductive assumption we have that M k , ⇡(m) |= , and M k , ⇡(i) |= ↵ for all 0  i < m. Now, consider the prefix ⇡ k of length k of ⇡. We have that ⇡ k 2 ⇧ k (s). Since m 2 I, by the definition of the bounded semantics we can conclude that M k , s |= E(↵U I ). 2. Let ' = E(↵R I ). From the unbounded semantics we have that there is a path ⇡ 2 ⇧(s) such that either (1) (8 m 2 I)M IS , ⇡(m) |= or (2) (9 m 2 I) (M IS , ⇡(m) |= ↵ and (8 0  i  m)M IS , ⇡(i) |= ). Let us consider the following cases: -Assume that (1) holds and I \ [0, k] = I. Thus, m  k for all m 2 I, and by the inductive assumption we have that M k , ⇡(m) |= for all m 2 I. Now, consider the prefix ⇡ k of length k of ⇡. We have that ⇡ k 2 ⇧ k (s). Thus, by the definition of the bounded semantics we can conclude that M k , s |= E(↵R I ). -Assume that (1) holds and I = [b, 1) for some b 0. Since the set of state of M IS is finite, we have that the path ⇡ must be an a-loop. Thus, we have that loop(⇡, b) 6 = ;. Since k = bmax{Max(BI(')), Max(UI('))}/ | M IS |c⇤ | M IS | + | M IS |, the prefix of ⇡ of the length k must belong to ⇧ k (s). Further, by the inductive assumption we have that M k , ⇡(m) |= for all b  m  k. Therefore, by the definition of the bounded semantics we have that M k , s |= E(↵R I ).

  bounded satisfaction is equivalent to the unbounded one. Theorem 1. Let M IS be a model associated to an interpreted system, M k its k-model, k = bmax{Max(BI(')), Max(UI('))}/ | M IS |c⇤ | M IS | + | M IS |, and ' a RTECTLK formula. Then, M IS |= ' iff M IS |= k '.

  j) |= and loop(⇡, left(I) + 1) 6 = ;) or (4) (8 left(I)  j  k)(M k , ⇡(j) |= and loop(⇡, left(I)) 6 = ;) .

4 î=0(

 4 ¬w 0,1 [i]) ^¬w 1,1 [0] ^w1,1 [1] ^4 î=2 (¬w 1,1 ) .

k

  , for k = 1, 2, . . ., according to the definition on page 173.

  the transitive closure of ⇠ E ), and ⇠ D def = T i2 ⇠ i . Definition 2. Let M IS be a model, s a state, and ↵, the RTECTLK formulae. M IS , s |= ↵ denotes that ↵ is true at the state s in the model M IS . The relation |= is defined inductively as follows: M

The propositional formula [M IS , '] k is defined over state variables w 0,0 , w n,m , for 0  m  k and 1  n  fk('). We start off with the definition of its first conjunct, i.e., the definition of [M ',◆ IS ] k , which constrains the f k (') symbolic k-paths to be valid k-path of M k . Namely,

The formula

, is inductively defined as follows:

]. This fully defines the encoding of the formula [M IS , '] k . Now we show that the validity of a RTECTLK formula ' on a submodel M 0 (s), defined by using the function f k , is equivalent to the satisfiability of the formula [M IS , '] k . Once we show this, we can conclude that the validity of ' on the model M IS is equivalent to the satisfiability of [M IS , '] k (see Theorem 3). Lemma 5. Let M IS be a model, M k its k-model, and ' a RTECTLK formula. For each state s of M IS , the following holds: ] k encodes f k (') symbolic k-paths to be valid k-paths of M k . Hence, there is a set of k-paths in M k , which satisfies the formula ' of size smaller or equal to f k ('). Thus, we conclude that there is a submodel M

The proof is by induction on the length of '. The lemma follows directly for the propositional variables and their negations. For ' = ↵ _ , ↵ ^ , EX↵ the proof is like in [START_REF] Penczek | Bounded Model Checking for the Universal Fragment of CTL[END_REF] (see Lemma 6.3). For epistemic operators, i.e., ' = K l ↵, E ↵, D ↵, C ↵, the proof is like in [START_REF] Penczek | Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking[END_REF] (see Lemma 3). Consider the following cases: