On the consistency of context-aware systems

1 Introduction

Context-aware systems are flexible and adaptable to the context of information [4]. Due to the inherent huge amount of context variables in these systems, developing a context-aware system tends to be a complex task for developers. In order to help reduce complexity and improve the maintenance and scalability in context-aware systems, it then is necessary to use modeling and reasoning techniques.

Basic modal logic K is an extension of propositional logic with necessity and possibility operators [5]. Many extensions of K, such as linear temporal logic (LTL), propositional dynamic logic (PDL), computational tree logic (CTL) and description logics (DLs), have been successfully used as reasoning frameworks in a wide range of domains, such as program analysis, knowledge representation, databases, programming languages.

Due to the well-known balance of expressive power and efficient reasoning algorithms associated to modal logics [11], we propose in the current work the use of expressive modal logics as a reasoning framework for context-aware pervasive systems. In particular, we propose a consistency model for a context-aware communication system. The system is composed of a set of users with communication preferences, and a set of locations with communications constraints. Location of users at different times are described in a schedule. Communication can be synchronous or asynchronous. The system is free of inconsistencies when users are able to communicate in spite of location and communication preferences and constraints. We characterize this consistency model in terms of the satisfiability of a μ-calculus (an expressive modal logic) formula. We show this characterization is correct and optimal. Also, an implementation is described and tested with several experiments.

2 A context-aware system

Following the description of the context-aware communication system [8], in this section, we define the notion of system consistency in terms of tree structures. We present the tree structure in the style of Kripke.

A tree structure K is defined as a tuple (N, R, L) where:

N is a set of nodes;

The input of the communication system consists of a set of user communication preferences, a set of location constraints, and a schedule that describing when users are at a specific location.

We present two types of communications that can be synchronous and asynchronous in a company. For instance, let say the communication system is composed of two users, whose communications preferences consist of e-mail and chat, and e-mail and phone, respectively. E-mail and chat and chat imply asynchronous communication and mobile call implies synchronous communication. It is then easy to see that user 1 can start communication asynchronously with user 2. However, it may be the case that according to the schedule, user 2 will be located at places where e-mail is not available. Furthermore, user 2 may have access to e-mail but only before user 1. In this two cases, we say the communication system is not consistent because constraints forbid communication. The μ-calculus formula characterizing the system is satisfiable, if and only if, the system is consistent.

Formally, we describe the input of the system as sets.

Definition 1. (System input)

The set of communication channels CH = {c₁, …, c _n } is divided in asynchronous AC and synchronous SC, that is, CH = AC ∪ SC and AC∩ SC = ∅.

Example 1.Now, we consider a company where it has several locations and two users need to communicate with each other. Users are in a different location (warehouse, office), therefore, they have to be in communication at some moment during the day.

We present the constraints, preferences and schedule where the user u _y arrives at t₁ to the warehouse and user u _c arrives at t₂ to the office also show user preferences and the location where they will be. We introduce the consistent system input.

The set of communication channels is CH = {mobilecall, landline, message}.

Now consider the inconsistent system input where the user u _y has not preferences. We are based on the previous sets, the inconsistent system is presented with the following sets:

The set of user preferences is PC = {(u _c , mobilecall), (u _c , message), (u _c , landline)}

In order to semantically define the consistency of the communication system, we define a consistency model.

Definition 2. (System consistency model) Given a set of communication channels CH, a set of user preferences PC, a set of location constraints PL, and a schedule SCH, we define the consistency model CModel (CH, PC, PL, SCH) (or simply CModel) as a tree structure (N, R, L), as follows:

there is one node for the root r ∈ L (n);

Intuitively, a consistency model is tree of 5 levels: the first level is the root; the second is composed by the time lapses considered in the schedule; the third level contains the locations; the communication channels available at a particular location compose the fourth level; the last level contains the users associated with each communication channel. In Fig. 1 it is depicted a graphical representation of a consistency communication model.

OPEN IN VIEWER

Fig.1

Graphical representation of a consistency communication model.

In order to define the consistency of the communication system, we define the following relations in a tree (N, R, L): a node n₁ is a child of a node n₂, written child (n₁, n₂), if and only if, R (n₁, 1) = n₂ or there is a non empty sequence R ( n 1 , 1 ) = n 1 ′ , R ( n 1 ′ , 2 ) = n 2 ′ , … , R ( n i ′ , 2 ) = n 2 ; a node n₁ is a descendant of a node n₂, written descendant (n₁, n₂), if and only if, there is a non empty sequence of nodes n 1 ′ , n 2 ′ , … , n i ′ , such that child ( n 1 , n 1 ′ ) , child ( n 1 ′ , n 2 ′ ) , …, child ( n i ′ , n 2 ) ; and a node n₂ is a following sibling of a node n₁, written fsibling (n₁, n₂), if and only if, n₁ is the same than n₂ or there is a (possibly empty) sequence of nodes R ( n 1 , 2 ) = n 1 ′ , …, R ( n i ′ , 2 ) = n 2 .

Definition 3. (System consistency) Given a consistency model CModel, we say user u₁ can communicate with user u₂, if and only if,

(Synchronously) there is a channel node n _c , such that child (n _c , n _{u 1} ) and child (n _c , n _{u 2} ), and there is a time node n _t , such that descendant (n _t , n _c ), descendant (n _t , n _{u 1} ) and descendant (n _t , n _{u 2} );

Synchronous communication among two users occurs in the system consistency model when the user nodes are children of the same communication channel node and descendants of same time node.

Asynchronous communication eliminates the time restriction: the user node who starts communication must be a descendant of a time node, which is a previous sibling of ancestor time node of the other user node.

Example 2. Consider the system input described in Example 1. Now we present CModel (CH, PC, PL, SCH).

The tree has a root (r).

In Fig. 2 is depicted the CModel for the consistent system with synchronous and asynchronous communication. Figure 3 is observed the CModel for the inconsistent system with synchronous and asynchronous communication. In this figure we observe that the user u _y does not appear in the CModel, this is because he has not preferences.

OPEN IN VIEWER

Fig.2

The CModel A is the synchronous communication, the formula is root ∧ N₁ (tc) ∧ SC (u _c , u _y ) and the CModel B is the asynchronous communication and the formula is root ∧ N₁ (t _c ) ∧ AC (u _c , u _y ). Where r is the root, c₁ is the mobile call, c₂ is landline, c₃ is the message, l₁ is the office and l₂ is the warehouse.

In this section, we characterize the notion of system consistency in terms of a logic formula of the μ-calculus with converse. Before defining the set of formulas, we consider a fixed alphabet composed of three sets PROP, MOD and Var, where PROP is a set of propositions, MOD = {1, 2, 3, 4} is a set of modalities, and Var is a set of variables.

Definition 4. (Syntax) The set of μ-calculus formulas is defined by the following grammar: φ : : = p ∣ X ∣ ¬ φ ∣ φ ∨ ψ ∣ 〈 m 〉 φ ∣ μ X . φ where p is a proposition, m a modality, and X is a variable.

We assume variables can only occur bounded and in the scope of a modality.

Formulas are interpreted as node subsets in unranked trees K = (N, R, L).

Definition 5. (Semantics) Consider a tree K and a valuation V : Var → 2 ^N . Formulas are interpreted as follows: 〚 p 〛 V K = { n ∣ p ∈ L ( n ) } 〚 ¬ φ 〛 V K = N ∖ 〚 φ 〛 V K 〚 φ ∨ ψ 〛 V K = 〚 φ 〛 V K ∪ 〚 ψ 〛 V K 〚 〈 m 〉 φ 〛 V K = { n ∣ R ( n , m ) ∩ 〚 φ 〛 V K ≠ ∅ } 〚 X 〛 V K = V ( X ) 〚 μ X . φ 〛 V K = ⋂ { N ′ ∣ 〚 φ 〛 V [ μ X . φ / X ] K ⊆ N ′ }

A formula φ is satisfiable, if and only if, there is a tree such as the interpretation of φ over the tree is not empty, that is 〚 φ 〛 V K ≠ ∅ . If a tree K satisfies a formula φ, we say K is a model of φ.

Intuitively, propositions are used as labels for nodes, negation (¬) is interpreted as set complement, disjunctions are interpreted as set union. Modal formulas 〈m〉φ hold in nodes where there is an m-adjacent node supporting φ. The least fixed-point is intuitively interpreted as a recursion operator.

Notation: φ ∧ φ : = ¬ (¬ φ ∨ ¬ φ), [m] φ : = ¬ 〈m〉 ¬ φ, νx. φ : = ¬ μx. ¬ φ [ ^x /_¬x], ⊤ : = p ∨ ¬ p, and ⊥ : =¬ ⊤, 〈m〉⁰φ : = φ, 〈m〉¹φ : = 〈m〉φ, 〈m〉 ⁱ φ : = 〈m〉^i-1〈m〉φ where i is the natural number.

We describe a characterization of the consistency model in terms of a μ-calculus formulas.

Definition 6. (Consistency formula) Given a system input CH, PC, PL and SCH, and a communication type tc ∈ {syn, asyn}, syn for synchronous and asyn for asynchronous, we define the consistency formula as follows: N 1 ( tc ) : = 〈 1 〉 ( t 1 ∧ N 2 ( tc , t 1 ) ∧ ⋀ i = 2 k 1 〈 2 〉 i - 1 ( t i ∧ N 2 ( tc , t i ) ) ∧ 〈 2 〉 k 1 - 1 ¬ 〈 2 〉 ⊤ ) N 2 ( tc , t ) : = 〈 1 〉 ( l 1 ∧ N 3 ( tc , t , l ) ∧ ⋀ i = 2 k 2 〈 2 〉 i - 1 ( l i ∧ N 3 ( tc , t , l ) ) ∧ 〈 2 〉 k 2 - 1 ¬ 〈 2 〉 ⊤ ) N 3 ( tc , t , l ) : = { ¬ 〈 1 〉 ⊤ h ( tc , t , l ) = 0 ) F 3 ( tc , t , l ) h ( tc , t , l ) ≥ 1 ) F 3 ( tc , t , l ) : = 〈 1 〉 ( c 1 ∧ N 4 ( tc , t , l , c 1 ) ∧ ⋀ i = 2 h ( tc , t , l ) 〈 2 〉 i - 1 ( c i ∧ N 4 ( tc , t , l , c i ) ) ∧ 〈 2 〉 h ( tc , t , l ) - 1 ¬ 〈 2 〉 ⊤ ) N 4 ( tc , t , l , c ) : = { ¬ 〈 1 〉 ⊤ k ( tc , t , l , c , u ) = 0 ) F 4 ( tc , t , l , c ) k ( tc , t , l , c , u ) ≥ 1 ) F 4 ( tc , t , l , c ) : = 〈 1 〉 ( u 1 ∧ ¬ 〈 # 1 〉 1 ⊤ ∧ ⋀ i = 2 k ( tc , t , l , c , u ) 〈 2 〉 i - 1 u i ∧ 〈 2 〉 k ( tc , t , l , c , u ) - 1 ¬ 〈 2 〉 ⊤ ) where k₁ is the number of time propositions in the schedule, k₂ is the number of locations, h (tc, t, l) = | {c ∈ tc ∣ (l, c) ∈ PL} | is the number of communication channels of type tc at a particular location l, and k (tc, t, l, c, p) = | {c ∈ tc ∣ (p, t, l) ∈ SCH, (p, c) ∈ PC} | is the number of users with a communication channel c as a preference.

Example 3. Consider again the CModel described in Example 2 and according to with Definition 6, we define N1 (syn) for the time where the users are in the company. N 1 ( t c ) : = t 1 ∧ N 2 ( t c , t 1 ) ∧ 〈 2 〉 ( t 2 ∧ N 2 ( t c , t 2 ) ) ∧ 〈 2 〉 〈 2 〉 ( t 3 ∧ N 2 ( t c , t 3 ) ) ∧ ¬ 〈 2 〉 〈 2 〉 〈 2 〉 ⊤

Given the three times of N₁, the locations are added for each of time. The second level is as follows: N 2 ( tc , t 1 ) : = 〈 1 〉 ( l 1 ∧ N 3 ( tc , t 1 , l 1 ) ∧ 〈 2 〉 ( l 2 ∧ N 3 ( tc , t 1 , l 2 ) ) ∧ ¬ 〈 2 〉 〈 2 〉 ⊤ ) N 2 ( tc , t 2 ) : = 〈 1 〉 ( l 1 ∧ N 3 ( tc , t 2 , l 1 ) ∧ 〈 2 〉 ( l 2 ∧ N 3 ( tc , t 2 , l 2 ) ) ∧ ¬ 〈 2 〉 〈 2 〉 ⊤ ) N 2 ( tc , t 3 ) : = 〈 1 〉 ( l 1 ∧ N 3 ( tc , t 3 , l 1 ) ∧ 〈 2 〉 ( l 2 ∧ N 3 ( tc , t 3 , l 2 ) ) ∧ 〈 2 〉 ¬ 〈 2 〉 ⊤ ) where N₃ is the available channel of the location, l₁ is office and l₂ is warehouse.

Given the locations of office and warehouse, the third level of a consistent system is the following. The communication system is using a synchronous communication channel. N 3 ( syn , t 1 , l 1 ) : = 〈 1 〉 ( ¬ ⊤ ) N 3 ( syn , t 1 , l 2 ) : = 〈 1 〉 ( c 1 ∧ N 4 ( syn , t 1 , l 2 , c 1 ) ∧ ¬ 〈 2 〉 ⊤ ) ⋮ N 3 ( syn , t 3 , l 2 ) : = 〈 1 〉 ( c 1 ∧ N 4 ( syn , t 3 , l 2 , c 1 ) ∧ ¬ 〈 2 〉 ⊤ )

The communication system is using a asynchronous communication channel. N 3 ( asyn , t 1 , l 1 ) : = 〈 1 〉 ( ¬ ⊤ ) N 3 ( asyn , t 1 , l 2 ) : = 〈 1 〉 ( c 3 ∧ N 4 ( asyn , t 1 , l 2 , c 3 ) ∧ ¬ 〈 2 〉 ⊤ ) ⋮ N 3 ( asyn , t 3 , l 2 ) : = 〈 1 〉 ( c 3 ∧ N 4 ( asyn , t 3 , l 2 , c 3 ) ∧ ¬ 〈 2 〉 ⊤ )

The third level of a inconsistent system. The system is using a synchronous communication channel. N 3 ( syn , t 1 , l 1 ) : = 〈 1 〉 ( ¬ ⊤ ) N 3 ( syn , t 1 , l 2 ) : = 〈 1 〉 ( ¬ ⊤ ) ⋮ N 3 ( syn , t 3 , l 2 ) : = 〈 1 〉 ( ¬ ⊤ )

The system is using a asynchronous communication channel. N 3 ( asyn , t 1 , l 1 ) : = 〈 1 〉 ( ¬ ⊤ ) N 3 ( asyn , t 1 , l 2 ) : = 〈 1 〉 ( ¬ ⊤ ) ⋮ N 3 ( asyn , t 3 , l 2 ) : = 〈 1 〉 ( ¬ ⊤ ) where c₁ is mobile call, c₂ is landline, c₃ is message, l₁ is the office and l₂ is the warehouse.

Now, we present the fourth level where the users are in the locations with the common channels between users and locations. The fourth level of a consistent system.

The system is using a synchronous communication channel. N 4 ( syn , t 1 , l 2 , c 1 ) : = 〈 1 〉 ( u y ∧ ¬ 〈 2 〉 ⊤ ) ⋮ N 4 ( syn , t 3 , l 2 , c 1 ) : = 〈 1 〉 ( u y ∧ ¬ 〈 2 〉 ⊤ )

The system is using a asynchronous communication channel. N 4 ( asyn , t 1 , l 2 , c 3 ) : = 〈 1 〉 ( u y ∧ ¬ 〈 2 〉 ⊤ ) ⋮ N 4 ( asyn , t 3 , l 3 , c 3 ) : = 〈 1 〉 ( u y ∧ ¬ 〈 2 〉 ⊤ )

The fourth level of a inconsistent system.

The system is using a synchronous communication channel. N 4 ( syn , t 2 , l 1 , c 1 ) : = 〈 1 〉 ( u c ∧ ¬ 〈 2 〉 ⊤ ) ⋮ N 4 ( syn , t 3 , l 1 , c 2 ) : = 〈 1 〉 ( u c ∧ ¬ 〈 2 〉 ⊤ )

The system is using a asynchronous communication channel. N 4 ( asyn , t 2 , l 1 , c 3 ) : = 〈 1 〉 ( u c ∧ ¬ 〈 2 〉 ⊤ ) N 4 ( asyn , t 3 , l 1 , c 3 ) : = 〈 1 〉 ( u c ∧ ¬ 〈 2 〉 ⊤ ) where c₁ is mobile call, c₂ is landline, c₃ is message, l₁ is the office and l₂ is the warehouse.

Lemma 1. Given a system input CH, PC, PL and SCH, [ [ # 1 ] ] # 3 # 2 N 1 ( tc ) ] CModel V ≠ ∅ , for any V. Furthermore, if there is a K such that [ [ # 1 ] ] # 3 # 2 N 1 ( tc ) ] K V ≠ ∅ , then K is the CModel.

Proof. We proceed by induction on the size of the sytem input.

The base case is when there is only 1 time in the schedule, and 1 location. There are two subcases, when there is one communication channel of type tc available at the location, and when there is not. For the last subcase, according to Definition 6: N 1 ( tc ) = 〈 # 1 〉 1 ( t 1 ∧ 〈 # 1 〉 1 ( l 1 ∧ ¬ 〈 # 1 〉 1 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤

According to Definition 2, CModel = (N, R, L) is then defined as: N = {r, n _{t 1} , n _{l 1,1} }, R = R¹ = {(r, n _{t 1} ), (n _{t 1} , n _{l 1,1} )}, and L (n _{t 1} ) = {t₁}, L (n _{l 1,1} ) = {l₁}. Which clearly satisfies N₁ (tc). For the first subcase, two additional cases arise: when there is one user with the communication channel among its preferences, and when there is not. For this last case: N 1 ( tc ) = 〈 # 1 〉 1 ( t 1 ∧ 〈 # 1 〉 1 ( l 1 ∧ 〈 # 1 〉 1 ( c 1 ∧ ¬ 〈 # 1 〉 1 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤

And the corresponding satisfying CModel = (N, R, L): N = {r, n _{t 1} , n _{l 1,1} , n _{c 1,1,1} }, R = R¹ = {(r, n _{t 1} ), (n _{t 1} , n _{l 1,1} ), (n _{l 1,1} , n _{c 1,1,1} )}, and L (n _{t 1} ) = {t₁}, L (n _{l 1,1} ) = {l₁}, L (n _{c 1,1,1} ) = c₁.

When there is one user with preference channel c₁, then: N 1 ( tc ) = 〈 # 1 〉 1 ( t 1 ∧ 〈 # 1 〉 1 ( l 1 ∧ 〈 # 1 〉 1 ( c 1 ∧ 〈 # 1 〉 1 ( u 1 ∧ ¬ 〈 # 1 〉 1 ⊤ ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤ ) ∧ ¬ 〈 # 1 〉 2 ⊤

The corresponding satisfying CModel is then:

CModel = (N, R, L): N = {r, n _{t 1} , n _{l 1,1} , n _{c 1,1,1} , n _{u 1,1,1,1} }, R = R¹ = {(r, n _{t 1} ), (n _{t 1} , n _{l 1,1} ), (n _{l 1,1} , n _{c 1,1,1} ), (n _{c 1,1,1} , n _{u 1,1,1,1} )}, and L (n _{t 1} ) = {t₁}, L (n _{l 1,1} ) = {l₁}, L (n _{c 1,1,1} ) = c₁, L (n _{u 1,1,1,1} ) = u₁.

For the induction step, assume there are k₁ time variables, k₂ locations, h (tc, t _i , l _j ) communication channels of type tc per location (i = 1, …, k₁,j = 1, …, k₂), respectively, and k (tc, t _i , l _j , u _m ) users per communication channel (m = 1, …, h (tc, t _i , l _j )), resp. Assume [ [ # 1 ] ] # 3 # 2 N 1 ′ ( tc ) CModel ′ V ≠ ∅ for some V, where CModel′ = (N′, R′, L′), where N 1 ′ ( tc ) and CModel′ corresponds to Definitions 2 and 6, resp. If the system input increases (k₁ + 1 time variables, k₂ + 1 locations, h (tc, t _i , l _j ) +1 communication channels, or k (tc, t _i , l _j , c _m ) +1 users), it is then clear that [ [ # 1 ] ] # 3 # 2 N 1 ( tc ) CModel V ≠ ∅ , where CModel is the resulted tree by updating CModel′ with the corresponding (according to Definition 2) additional nodes, and N₁ (tc) is the resulted formula by updating N 1 ′ ( tc ) with the corresponding (according to Definition 6) conjunctions.

The second condition of the lemma goes straightforward by contradiction, that is, we assume [ [ # 1 ] ] # 3 # 2 N 1 ( tc ) K V ≠ ∅ and K is not the CModel. □

We now define a characterization formula for each type of communication.

Definition 7. (Synchronous communication) The characterization formula SC (u₁, u₂) corresponding to a synchronous communication from user u₁ to u₂ is defined as follows: SC ( u 1 , u 2 ) : = ⋁ i = 1 k F SC ( u 1 , u 2 , c i ) F SC ( u 1 , u 2 , c i ) : = 〈 1 〉 ( μ T . ( 〈 1 〉 ( F ( u 1 , c i ) ∧ F ( u 2 , c i ) ) ∨ 〈 2 〉 T ) ) F ( u , c ) : = μ L . ( 〈 1 〉 ( μ C . ( c ∧ 〈 1 〉 ( μ P . u ∨ 〈 2 〉 P ) ) ∨ 〈 2 〉 C ) ) ∨ 〈 2 〉 L ) where k is the number of synchronous communication channels.

Example 4.Consider the CModel described in Example 3, now we presented a query in the communication system where if a user u _c wishes to contact the user u _y , then, according to Definition 7 we present an example of synchronous communication. F SC ( u c , u y , c 1 ) : = 〈 1 〉 ( μ T . ( 〈 1 〉 ( F ( u c , c 1 ) ∧ F ( u y , c 1 ) ∨ 〈 2 〉 T ) ) SC ( u c , u y ) : = F SC ( u c , u y , c 1 ) where c₁ is mobile call.

In this example shows the mobile call channel because this channel is only in common for the two users. In this case, it is possible to communicate between the two users, the consistent CModel is presented in Fig. 2 and in the case where the user does not have preferences, the communication system is inconsistent and the inconsistent CModel is presented in Fig. 3. In row one of Table 4, we show the execution time for users u _y and u _c .

OPEN IN VIEWER

Fig.3

The inconsistent CModel A is the synchronous communication, the formula is root ∧ N₁ (tc) ∧ SC (u _c , u _y ) and the inconsistent CModel B is the asynchronous communication and the formula is root ∧ N₁ (t _c ) ∧ AC (u _c , u _y ). Where r is the root, c₁ is the mobile call, c₂ is landline, c₃ is the message, l₁ is the office and l₂ is the warehouse.

Definition 8. (Asynchronous communication) The characterization formula AC (u₁, u₂) corresponding to a synchronous communication from user u₁ to u₂ is defined as follows: AC ( u 1 , u 2 ) : = ⋁ i = 1 k F AC ( u 1 , u 2 , c i ) F AC ( u 1 , u 2 , c i ) : = 〈 1 〉 ( μ T . ( 〈 1 〉 F ( u 1 , c i ) ∧ μ T ′ . ( 〈 1 〉 F ( u 2 , c i ) ∨ 〈 2 〉 T ′ ) ∨ 〈 2 〉 T ) ) where k is the number of asynchronous channels and F is defined in Definition 7.

Example 5. Consider again the CModel described in Example 3, when the user u _c wishes to contact the user u _y . Now the communication asynchronous of two people are as follows: F AC ( u c , u y , c 3 ) : = 〈 1 〉 ( μ T . ( 〈 1 〉 F ( u c , c 3 ) ∧ μ T ′ . ( 〈 1 〉 F ( u y , c 3 ) ∨ 〈 2 〉 T ′ ) ∨ 〈 2 〉 T ) ) AC ( u c , u y ) : = F AC ( u c , u y , c 3 ) where c₃ is message.

Example 6. Now we present another example of a communication system with 4 users, 6 channels, 6 locations and 6 times. Table 1 shows restrictions of the location where the locations L₁, L₄, and L₆ are offices, location L₃ is the conference room and location L₂ and L₅ are warehouses, in Table 2 shows the users preferences, and Table 3 shows the schedule where the users U₁, U₂ and U₃ are in the times T₁ to T₄, and user U₄ is from time T₃ to T₅.

In this communication system, the consistency is identified when 2 users or more within the company need communicate. In this case, the user U₁ needs to communicate with the user U₂, the user U₃ with U₄. For this example, the users must have a communication during the day. In a real situation, if a user can not communicate, then, the system should notify him that the preferences or schedule are not appropriate.

Table 4 shows the execution time for users U₁ and U₂ in row two where communication between them is possible for synchronous and asynchronous channels, but in the case where the users U₃ and U₄ wish to communicate is not possible for synchronous and asynchronous channels, then, the communication system is inconsistent for the users U₃ and U₄.

Lemma 2. Consider a system input CH, PC, PL and SCH. User u₁ can communicate with user u₂ (a)synchronously, if and only if, [ [ # 1 ] ] # 3 # 2 SC ( u 1 , u 2 ) CModel V ≠ ∅ or [ [ # 1 ] ] # 3 # 2 AC ( u 1 , u 2 ) CModel V ≠ ∅ , respectively, for any V.

Proof. For synchronous communication. It is straight forward by the following immediate facts, for i = 1, 2:

child (n _c , n _{u i} ) holds in CModel, if and only if, c ∧ 〈 # 1 〉 1 (μP. u _i  ∨ 〈 # 1 〉 2P) is satisfied by CModel;

For asynchronous communication the proof is analogous. □

Theorem 1. Given a system input CH, PC, PL and SCH, user u₁ can consistently communicate with user u₂, if and only if, there is a tree structure K, such that [ [ # 1 ] ] # 3 # 2 N 1 ( tc ) ∧ SC ( u 1 , u 2 ) K V ≠ ∅ , for any V. Furthermore, consistent communication is in EXPTIME with respect to the system input.

Proof. The first part of the Theorem is immediate from Lemmas 1 and 2. EXPTIME complexity comes from the EXPTIME-Completeness of μ-calculus satisfiability [11], and that the size of N₁ (tc) ∧ SC (u₁, u₂) is polynomial with respect to the system input size. □

In this section, the experiments were carried out in a computer with the following features: Windows 8 operating system, AMD processor A6 2.7 GHz, 8 GB of RAM. This algorithm is online in the following url https://148.226.81.4:8181/AlgoritmoWeb/

In this work, we used for the experiments an implementation of satisfiability algorithm of μ-calculus [9]. In these experiments, considering the system input described in Definition 2, that given a set of communication channels, a set of user preferences, a set of constraints and schedule, we analyzed the consistency of the communication system, for which it was used the satisfiability algorithm of μ-calculus for identifying consistency of communication system, where if the algorithm returns true then the system is consistent but when it returns false then the system is inconsistent. Now for the following experiments, the evaluation time is in milliseconds.

Table 4 shows the system input in the columns U, L, Channels and T, where U is the number of users, L is the number of locations, the next two columns (Channels) are the number of channels for synchronous and asynchronous communication and T is the number of times. The next two columns are the CModel evaluation for the channel of communication synchronous and asynchronous, this is the satisfiability of N₁. The following four columns are consistent and inconsistent queries for synchronous and asynchronous communication channels. Finally, the last two columns are the number of nodes in the CModel for synchronous and asynchronous channels.

In Example 1, the communication system is consistent since the two users can communicate. Also, Table 4 shows the experiments when a user has no preferences (row one).

Now, in Example 6, the communication system is consistent for the users U₁ and U₂ because can be communicated, but the users U₃ and U₄ have not communication, so when somebody will implement the reasoner in a communication system, this could notify the inconsistency of system when the users are declaring their preferences (row two).

Table 4 shows the experiments where these show different inputs of the communication system. We observed that the query does not increase the execution time. Also, if CModel has a higher number of nodes, then execution time of CModel is higher. Table 4 shows the system input where if we increase the number of users or the time, then the execution time has a polynomial increase, this can be observed in experiments 19, 20, 21 and 22. When we have a greater number of users, this generates more execution time because the algorithm performs a depth-first search in CModel. In another case when we increase the number of times, then, the CModel increases the size of nodes because the locations are repeated in each time, this case increases of execution time. We presented experiments with at least 20 users and 20 locations where the evaluation time is 12 seconds in synchronous communication and 25 seconds in asynchronous communication and the model size is 617 and 603 nodes, it shows in row 11. In CModel, the increment of locations is not relevant since if the users are not added to the location then this branch of CModel is truncated.

We propose this reasoner for communication systems where communication is synchronous, this is because only the current time would be evaluated. This gives the possibility of implementation in a real-time system.

5 Conclusions

In this paper, we proposed the used the propositional μ-calculus with converse as a modeling language for context-aware systems. In particular, we described a notion of consistency for a context-aware communication system. In a consistent system, users are able to communicate, synchronously or asynchronously, in spite of a set of communication, location and time constraints. Consistency is characterized in terms of the satisfiability of a μ-calculus formula. We tested the efficiency of this characterization with a recent implementation of a μ-calculus satisfiability algorithm [9]. Several experiments are described. We tested up to 30 users and 30 locations.

As further research perspectives, we aim to develop efficient reasoning algorithms for more expressive specification languages, such as the ones with arithmetic constructors [5]. We believe these arithmetic constructors can be used to model more complex space constraints in context-aware systems [2].