On the consistency of context-aware systems

Abstract

Context-aware systems are ubiquitous computing systems capable to adapt themselves to a dynamically changing environment. Ensuring consistency in context-aware systems has proved a challenging task due to the inherent expressive power required to model dynamical systems. In the current work, we propose the use of the μ-calculus with converse, an expressive modal logic, for modeling and verifying consistency. In particular, we propose a consistency model for a context-aware communication system. Consistency is tested in terms of the satisfiability of a μ-calculus formula. We show this consistency verification method is correct and a complexity analysis is provided. We also describe an implementation with several experiments.

Keywords

Context-aware systems automated reasoning modal logics

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.

1.1 Related works and motivation

The context-aware communication system described in this work is inspired from the one introduced in [4, 8]. In contrast with [4, 8], where a communication recommendation results from a set of user and location communication constraints (preferences), in our proposal, the system is verified and consistency is guaranteed, that is, users communication capability is tested in the setting of location and communication constraints. Furthermore, the communication system described in the current paper considers also a time schedule for each user, verifying also asynchronous communication. These types of time constraints were not modeled in the approaches followed in [4, 8], due to the well-known hierarchical specification limitations of the modeling language CML (Context Modeling Language).

Other approaches for modeling of context-aware systems are those who can model space constraints. These models can be expressed as [3]: where you are, who you are with and what resources are nearby. There are different types of spatial modeling such as set-based, hierarchical, graph-based, and hybrid. In the current proposal, locations are modeled symbolically by logic propositions. In contrast with known space modeling approaches [3, 4], one major feature of the consistency model described in the current work is that time and space constraints are modeled in a sole verification framework.

Ontologies have been also successfully used as a modeling language for context-aware systems [6, 10, 12]. In particular, in [1] several intelligent environments are modeled and simulated by means of an OWL 2 (Web Ontology Language) reasoning framework. Space modeling is a known limitation of ontology frameworks [4]. This is due to the expressiveness limitations associated with the corresponding efficient reasoning algorithms in description logics. The μ-calculus may expressive description logics [11]. In the current proposal, we use an efficient implementation of a μ-calculus reasoning algorithm [9] to test the consistency model.

In [7], it is described a modeling and verification framework for context-aware systems. The modeling part of this framework is based on Model Driven Engineering (MDE), and the verification part is based on the model checking of Linear Temporal Logic (LTL) formulas. System invariants are generated from the MDE model, then these invariants are tested by the Maude LTL model checker. The expressive power of the modeling language used in our proposal, μ-calculus, which also subsumes LTL, allows to describe more complex specification invariants, such as the consistency notion proposed in the current paper, which involves non-linear tree-shaped models, and time and location constraints.

1.2 Outline

In Section 2, we describe the communication system, their input and define the consistency system. In Section 3, we introduce the μ-calculus with converse modalities, defined the consistency formula and queries of the communication system. We present the experiments in Section 4 and finally, in Section 5 we present the conclusions.

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;

R is a family of binary relations R^m among nodes (N × N) forming a tree, that is, R¹ denotes the first child relation, R² the following (right) sibling, R³ the parent, and R⁴ the previous (left) sibling, we often write n′ ∈ R (n, m) instead of (n, n′) ∈ R^m; and

L is a function labeling L : N → 2^PROP, where PROP is a set of proposition variables.

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 = ∅.

The set of user preferences (restrictions) PC is composed of pairs (u, c), where u is a proposition naming an user, and c is a proposition used to name a communication channel.

The set of communication constraints for locations PL is composed of pairs (l, c), where l is a proposition naming a location and c is a proposition for a communication channel.

The schedule is defined as the set: SCH composed by triples (u, t, l), where u is a proposition for a user, t is a proposition for a particular time, l is a proposition for a location.

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}.

The set of user preferences is PC = {(u_y, mobile call), (u_y, message), (u_c, mobile call), (u_c, message), (u_c, landline)}

The set of constraints is PL = {(warehouse, mobile call), (warehouse, message), (office, mobile call), (office, landline), (office, message)}

The schedule is the following set: SCH = {(u_y, t₁, warehouse), (u_y, t₂, warehouse), (u_y, t₃, warehouse), (u_c, t₂, office), (u_c, t₃, office)}

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);

one node for each time proposition t_i ∈ L (n_{t
_i}) (i = 1, …, k₁), which are the children of the root, that is, R (n, 1) = n_t
₁, R (n_{t
_j}, 2) = n_{t
_j+1} (j = 1, …, k₁ - 1);

each time node has one child per location, that is, l_j ∈ L (n_{l
_i,j}) and R (n_{t
_i}, 1) = n_{l
_i,1} and R (n_{l_j,s,2}) = n_j,s+1, where i = 1, …, k₁, j = 1, …, k₂ and s = 1, …, k₂ - 1;

each location node has one child per channel available, that is, c_s ∈ L (n_i,j,w), R (n_{l
_i,j}, 1) = n_{c
_i,j,1} and R (n_{c
_i,j,w}, 2) = n_{c
_i,j,w+1}, where i = 1, …, k₁, j = 1, …, k₂, s = 1, …, k₃ and w = 1, …, k₃ - 1; and

each channel node has one child per user with that channel preference, that is, u_w ∈ L (n_{c
_i,j,s}), R (n_{c
_i,j,s}, 1) = n_{u
_i,j,1} and R (n_{u
_i,j,z}, 2) = n_{u
_i,j,z}, where i = 1, …, k₁, j = 1, …, k₂, s = 1, …, k₃, w = 1, …, k₄ and z = 1, …, k₄ - 1.

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.

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}^{'}, \dots, 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}^{'}, \dots, 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
₁) and child (n_c, n_u
₂), and there is a time node n_t, such that descendant (n_t, n_c), descendant (n_t, n_u
₁) and descendant (n_t, n_u
₂);

(Asynchronously) there is a channel node n_c, such that child (n_c, n_u
₁) and child (n_c, n_u
₂), and there are two time nodes n_t
₁ and n_t
₂, such that fsibling (n_t
₁, n_t
₂), descendant (n_t
₁, n_c), descendant (n_t
₂, n_c), descendant (n_t
₁, n_u
₁) and descendant (n_t
₂, n_u
₂).

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).

The time nodes are three t₁, t₂ and t₃ children of r.

Each time node has two child nodes office and warehouse.

Each location node has two synchronous channels (mobile call and landline) and an asynchronous channel (message).

Each channel node has one user (u_y and u_c), which are essential to the user’s preference.

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.

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.

3 Logic-based consistency

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 ∣ \neg φ ∣ φ \lor ψ ∣ 〈 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: $\begin{matrix} 〚 p 〛_{V}^{K} & = & {n ∣ p \in L (n)} \\ 〚 \neg φ 〛_{V}^{K} & = & N ∖ 〚 φ 〛_{V}^{K} \\ 〚 φ \lor ψ 〛_{V}^{K} & = & 〚 φ 〛_{V}^{K} \cup 〚 ψ 〛_{V}^{K} \\ 〚〈 m 〉 φ 〛_{V}^{K} & = & {n ∣ R (n, m) \cap 〚 φ 〛_{V}^{K} \neq \emptyset} \\ 〚 X 〛_{V}^{K} & = & V (X) \\ 〚 μ X . φ 〛_{V}^{K} & = & ⋂ {N^{'} ∣ 〚 φ 〛_{V [^{μ X . φ} /_{X}]}^{K} \subseteq N^{'}} \end{matrix}$

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} \neq \emptyset$ . 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: $\begin{matrix} N_{1} (tc) & : = & 〈 1 〉 (t_{1} \land N_{2} (tc, t_{1}) \land ⋀_{i = 2}^{k_{1}} 〈 2 〉^{i - 1} \\ (t_{i} \land N_{2} (tc, t_{i})) \land 〈 2 〉^{k_{1} - 1} \neg 〈 2 〉 ⊤) \\ N_{2} (tc, t) & : = & 〈 1 〉 (l_{1} \land N_{3} (tc, t, l) \land ⋀_{i = 2}^{k_{2}} 〈 2 〉^{i - 1} \\ (l_{i} \land N_{3} (tc, t, l)) \land 〈 2 〉^{k_{2} - 1} \neg 〈 2 〉 ⊤) \\ N_{3} (tc, t, l) & : = & {\begin{matrix} \neg 〈 1 〉 ⊤ & h (tc, t, l) = 0) \\ F_{3} (tc, t, l) & h (tc, t, l) \geq 1) \end{matrix} \\ F_{3} (tc, t, l) & : = & 〈 1 〉 (c_{1} \land N_{4} (tc, t, l, c_{1}) \land \\ ⋀_{i = 2}^{h (tc, t, l)} 〈 2 〉^{i - 1} (c_{i} \land N_{4} (tc, t, l, c_{i})) \\ \land 〈 2 〉^{h (tc, t, l) - 1} \neg 〈 2 〉 ⊤) \\ N_{4} (tc, t, l, c) & : = & {\begin{matrix} \neg 〈 1 〉 ⊤ & k (tc, t, l, c, u) = 0) \\ F_{4} (tc, t, l, c) & k (tc, t, l, c, u) \geq 1) \end{matrix} \\ F_{4} (tc, t, l, c) & : = & 〈 1 〉 (u_{1} \land \neg 〈 # 1 〉 1 ⊤ \land ⋀_{i = 2}^{k (tc, t, l, c, u)} 〈 2 〉^{i - 1} \\ u_{i} \land 〈 2 〉^{k (tc, t, l, c, u) - 1} \neg 〈 2 〉 ⊤) \end{matrix}$ 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. $\begin{matrix} N_{1} (t_{c}) & : = & t_{1} \land N_{2} (t_{c}, t_{1}) \land 〈 2 〉 (t_{2} \land N_{2} (t_{c}, t_{2})) \land \\ 〈 2 〉〈 2 〉 (t_{3} \land N_{2} (t_{c}, t_{3})) \land \neg 〈 2 〉〈 2 〉〈 2 〉 ⊤ \end{matrix}$

Given the three times of N₁, the locations are added for each of time. The second level is as follows: $\begin{matrix} N_{2} (tc, t_{1}) & : = & 〈 1 〉 (l_{1} \land N_{3} (tc, t_{1}, l_{1}) \land 〈 2 〉 (l_{2} \land \\ N_{3} (tc, t_{1}, l_{2})) \land \neg 〈 2 〉〈 2 〉 ⊤) \\ N_{2} (tc, t_{2}) & : = & 〈 1 〉 (l_{1} \land N_{3} (tc, t_{2}, l_{1}) \land 〈 2 〉 (l_{2} \land \\ N_{3} (tc, t_{2}, l_{2})) \land \neg 〈 2 〉〈 2 〉 ⊤) \\ N_{2} (tc, t_{3}) & : = & 〈 1 〉 (l_{1} \land N_{3} (tc, t_{3}, l_{1}) \land 〈 2 〉 (l_{2} \land \\ N_{3} (tc, t_{3}, l_{2})) \land 〈 2 〉 \neg 〈 2 〉 ⊤) \end{matrix}$ 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. $\begin{matrix} N_{3} (syn, t_{1}, l_{1}) & : = & 〈 1 〉 (\neg ⊤) \\ N_{3} (syn, t_{1}, l_{2}) & : = & 〈 1 〉 (c_{1} \land N_{4} (syn, t_{1}, l_{2}, c_{1}) \land \\ \neg 〈 2 〉 ⊤) \\ ⋮ \\ N_{3} (syn, t_{3}, l_{2}) & : = & 〈 1 〉 (c_{1} \land N_{4} (syn, t_{3}, l_{2}, c_{1}) \\ \land \neg 〈 2 〉 ⊤) \end{matrix}$

The communication system is using a asynchronous communication channel. $\begin{matrix} N_{3} (asyn, t_{1}, l_{1}) & : = & 〈 1 〉 (\neg ⊤) \\ N_{3} (asyn, t_{1}, l_{2}) & : = & 〈 1 〉 (c_{3} \land N_{4} (asyn, t_{1}, l_{2}, c_{3}) \\ \land \neg 〈 2 〉 ⊤) \\ ⋮ \\ N_{3} (asyn, t_{3}, l_{2}) & : = & 〈 1 〉 (c_{3} \land N_{4} (asyn, t_{3}, l_{2}, c_{3}) \\ \land \neg 〈 2 〉 ⊤) \end{matrix}$

The third level of a inconsistent system. The system is using a synchronous communication channel. $\begin{matrix} N_{3} (syn, t_{1}, l_{1}) & : = & 〈 1 〉 (\neg ⊤) \\ N_{3} (syn, t_{1}, l_{2}) & : = & 〈 1 〉 (\neg ⊤) \\ ⋮ \\ N_{3} (syn, t_{3}, l_{2}) & : = & 〈 1 〉 (\neg ⊤) \end{matrix}$

The system is using a asynchronous communication channel. $\begin{matrix} N_{3} (asyn, t_{1}, l_{1}) & : = & 〈 1 〉 (\neg ⊤) \\ N_{3} (asyn, t_{1}, l_{2}) & : = & 〈 1 〉 (\neg ⊤) \\ ⋮ \\ N_{3} (asyn, t_{3}, l_{2}) & : = & 〈 1 〉 (\neg ⊤) \end{matrix}$ 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. $\begin{matrix} N_{4} (syn, t_{1}, l_{2}, c_{1}) & : = & 〈 1 〉 (u_{y} \land \neg 〈 2 〉 ⊤) \\ ⋮ \\ N_{4} (syn, t_{3}, l_{2}, c_{1}) & : = & 〈 1 〉 (u_{y} \land \neg 〈 2 〉 ⊤) \end{matrix}$

The system is using a asynchronous communication channel. $\begin{matrix} N_{4} (asyn, t_{1}, l_{2}, c_{3}) & : = & 〈 1 〉 (u_{y} \land \neg 〈 2 〉 ⊤) \\ ⋮ \\ N_{4} (asyn, t_{3}, l_{3}, c_{3}) & : = & 〈 1 〉 (u_{y} \land \neg 〈 2 〉 ⊤) \end{matrix}$

The fourth level of a inconsistent system.

The system is using a synchronous communication channel. $\begin{matrix} N_{4} (syn, t_{2}, l_{1}, c_{1}) & : = & 〈 1 〉 (u_{c} \land \neg 〈 2 〉 ⊤) \\ ⋮ \\ N_{4} (syn, t_{3}, l_{1}, c_{2}) & : = & 〈 1 〉 (u_{c} \land \neg 〈 2 〉 ⊤) \end{matrix}$

The system is using a asynchronous communication channel. $\begin{matrix} N_{4} (asyn, t_{2}, l_{1}, c_{3}) & : = & 〈 1 〉 (u_{c} \land \neg 〈 2 〉 ⊤) \\ N_{4} (asyn, t_{3}, l_{1}, c_{3}) & : = & 〈 1 〉 (u_{c} \land \neg 〈 2 〉 ⊤) \end{matrix}$ 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 \neq \emptyset$ , for any V. Furthermore, if there is a K such that ${[[# 1]]}_{# 3}^{# 2} N_{1} (tc)] K V \neq \emptyset$ , 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: $\begin{matrix} N_{1} (tc) & = & 〈 # 1 〉 1 (t_{1} \land 〈 # 1 〉 1 (l_{1} \land \neg 〈 # 1 〉 1 ⊤) \land \\ \neg 〈 # 1 〉 2 ⊤) \land \neg 〈 # 1 〉 2 ⊤ \end{matrix}$

According to Definition 2, CModel = (N, R, L) is then defined as: N = {r, n_{t
₁}, n_{l
_1,1}}, R = R¹ = {(r, n_{t
₁}), (n_{t
₁}, n_{l
_1,1})}, and L (n_{t
₁}) = {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: $\begin{matrix} N_{1} (tc) & = & 〈 # 1 〉 1 (t_{1} \land 〈 # 1 〉 1 (l_{1} \land 〈 # 1 〉 1 (c_{1} \land \neg 〈 # 1 〉 1 ⊤) \land \\ \neg 〈 # 1 〉 2 ⊤) \land 〈 # 1 〉 2 ⊤) \land \neg 〈 # 1 〉 2 ⊤ \end{matrix}$

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

When there is one user with preference channel c₁, then: $\begin{matrix} N_{1} (tc) & = & 〈 # 1 〉 1 (t_{1} \land 〈 # 1 〉 1 (l_{1} \land 〈 # 1 〉 1 (c_{1} \land 〈 # 1 〉 1 (u_{1} \land \\ \neg 〈 # 1 〉 1 ⊤ \land \neg 〈 # 1 〉 2 ⊤) \land \neg 〈 # 1 〉 2 ⊤) \land \\ \neg 〈 # 1 〉 2 ⊤) \land \neg 〈 # 1 〉 2 ⊤) \land \neg 〈 # 1 〉 2 ⊤ \end{matrix}$

The corresponding satisfying CModel is then:

CModel = (N, R, L): N = {r, n_{t
₁}, n_{l
_1,1}, n_{c
_1,1,1}, n_{u
_1,1,1,1}}, R = R¹ = {(r, n_{t
₁}), (n_{t
₁}, 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
₁}) = {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 \neq \emptyset$ 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 \neq \emptyset$ , 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 \neq \emptyset$ 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: $\begin{matrix} 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}) \land \\ F (u_{2}, c_{i})) \lor 〈 2 〉 T)) \\ F (u, c) & : = & μ L . (〈 1 〉 (μ C . (c \land 〈 1 〉 (μ P . u \\ \lor 〈 2 〉 P)) \lor 〈 2 〉 C)) \lor 〈 2 〉 L) \end{matrix}$ 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. $\begin{matrix} F_{SC} (u_{c}, u_{y}, c_{1}) & : = & 〈 1 〉 (μ T . (〈 1 〉 (F (u_{c}, c_{1}) \land \\ F (u_{y}, c_{1}) \lor 〈 2 〉 T)) \\ SC (u_{c}, u_{y}) & : = & F_{SC} (u_{c}, u_{y}, c_{1}) \end{matrix}$ 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.

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: $\begin{matrix} 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}) \land \\ μ T^{'} . (〈 1 〉 F (u_{2}, c_{i}) \lor 〈 2 〉 T^{'}) \\ \lor 〈 2 〉 T)) \end{matrix}$ 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: $\begin{matrix} F_{AC} (u_{c}, u_{y}, c_{3}) & : = & 〈 1 〉 (μ T . (〈 1 〉 F (u_{c}, c_{3}) \land \\ μ T^{'} . (〈 1 〉 F (u_{y}, c_{3}) \lor 〈 2 〉 T^{'}) \\ \lor 〈 2 〉 T)) \\ AC (u_{c}, u_{y}) & : = & F_{AC} (u_{c}, u_{y}, c_{3}) \end{matrix}$ 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₅.

Table 1

Location constraints

Location	Synchronous	Asynchronous
L ₁	mobile call, landline	message
L ₂	mobile call	message
L ₃	mobile call, landline, video call	message, e-mail, voicemail
L ₄	mobile call, landline	message
L ₅	mobile call	message
L ₆	mobile call, landline	message, e-mail

Table 2

Preferences of the user

User	Synchronous	Asynchronous
U ₁	mobile call	message
U ₂	mobile call, landline	message
U ₃	landline	e-mail, voicemail
U ₄	mobile call, landline video call	message, e-mail

Table 3

Schedule

User	Location	Time
U ₁	L ₂	t ₁
U ₁	L ₂	t ₂
U ₁	L ₂	t ₃
U ₁	L ₆	t ₄
U ₂	L ₁	t ₁
U ₂	L ₃	t ₂
U ₂	L ₃	t ₃
U ₂	L ₄	t ₄
U ₃	L ₅	t ₁
U ₃	L ₅	t ₂
U ₃	L ₅	t ₃
U ₃	L ₁	t ₄
U ₄	L ₄	t ₃
U ₄	L ₄	t ₄
U ₄	L ₆	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₄.

Table 4

Evaluation time of the communication system

No.	U	L	Channels		T	CModel		Consistent query		Inconsistent query		Nodes
			syn	asyn		syn	asyn	syn	asyn	syn	asyn	syn	asyn
1	2	2	2	1	3	32	22	34	38	15	9	24	20
2	4	6	3	3	5	99	84	70	53	54	69	76	59
3	6	6	3	3	5	92	86	84	79	68	84	88	73
4	8	6	3	3	5	100	92	112	82	100	65	112	80
5	4	8	3	3	5	151	109	157	108	158	162	90	69
6	6	8	3	3	5	115	82	114	169	131	143	122	98
7	4	6	3	3	6	111	98	153	99	115	160	87	76
8	4	6	3	3	7	131	170	176	280	156	164	98	81
9	6	6	3	3	8	210	195	279	271	253	200	133	119
10	10	10	10	10	8	1258	1385	1337	1388	1141	1124	313	301
11	20	20	15	15	8	15220	24552	12107	25335.0	11176	16110	617	603
12	4	6	6	—-	1	114	—-	216	—-	50	—-	24	—-
13	10	6	6	—-	1	153	—-	218	—-	49	—-	32	—-
14	15	6	6	—-	1	278	—-	269	—-	46	—-	37	—-
15	4	10	6	—-	1	170	—-	205	—-	22	—-	28	—-
16	4	15	6	—-	1	203	—-	192	—-	164	—-	33	—-
17	4	6	10	—-	1	126	—-	394	—-	86	—-	32	—-
18	4	6	15	—-	1	283	—-	470	—-	188	—-	42	—-
19	10	10	10	—-	1	220	—-	118	—-	200	—-	40	—-
20	15	15	15	—-	1	477	—-	683	—-	465	—-	55	—-
21	20	20	15	—-	1	1250	—-	1202	—-	1332	—-	78	—-
22	30	30	15	—-	1	8698	—-	13868	—-	9078	—-	124	—-

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 \neq \emptyset$ or ${[[# 1]]}_{# 3}^{# 2} AC (u_{1}, u_{2}) CModel V \neq \emptyset$ , 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;

descendant (n_t, n_c) holds in CModel, if and only if, t ∧ 〈 # 1 〉 1 (μL. (〈 # 1 〉 1 (μC. c ∨ 〈 # 1 〉 2C) ∨ 〈 # 1 〉 2L)) is satisfied by CModel; and

descendant (n_t, n_{u
_i}) holds in CModel, if and only if, t ∧ 〈 # 1 〉 1 (μL. (〈 # 1 〉 1 (μC. 〈 # 1 〉 1 (μP. u_i ∨ 〈 # 1 〉 2P) ∨ 〈 # 1 〉 2C) ∨ 〈 # 1 〉 2L)) 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) \land SC (u_{1}, u_{2}) K V \neq \emptyset$ , 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. □

4 Experiments

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].

References

Baader

, Horrocks

and Sattler

, Description Logics, Handbook on Ontologies, Steffen Staab and Rudi Studer, International Handbooks on Information SystemsSpringer, (2009), pp21–43.

Bárcenas

, Molero

, Sánchez

, Benítez-Guerrero

and Mezura-Godoy

, Reasoning on expressive description logics with arithmetic constraint, IEEE, International Conference on Electronics, Communications and Computers2016.

Becker

and Dürr

, On location models for ubiquitous computing, Personal and Ubiquitous Computing9(1) (2005), 20–31.

Bettini

, Brdiczka

, Henricksen

, Indulska

, Nicklas

, Ranganathan

and Riboni

, A survey of context modeling and reasoning techniques, Pervasive and mobile computing, Elsevier (2010), pp 161–180.

Blackburn

and van Benthem

J.F.

, and Wolter

, Handbook of modal logic, Pervasive and mobile computingElsevier2006.

Chen

, Perich

, Finin

T.W.

and Joshi

, SOUPA: Standard ontology for ubiquitous and pervasive applications, In 1st Annual International Conference on Mobile and Ubiquitous Systems (MobiQuitous), IEEE Computer Society (2004), 258–267.

Djoudi

, Bouanaka

and Zeghib

, A formal framework for context-aware systems specification and verification, Journal of Systems and Software, IEEE122 (2016), 445–462.

Henricksen

and Indulska

, Developing context-aware pervasive computing applications: Models and approach,, Pervasive and mobile computingElsevier (2006), pp. 37–64.

Limón

, Bárcenas

, Benítez-Guerrero

and Medina

M.A.

, Depth-first reasoning on trees, Computación y SistemasIn Press, 2018.

10.

Riboni

and Bettini

, OWL 2 modeling and reasoning with complex human activities, Pervasive and Mobile Computing7(3) (2011), 379–395.

11.

, Vardi, Why is Modal Logic So Robustly Decidable? Descriptive Complexity and Finite Models, Immerman

Neil

and Phokion

G. Kolaitis

, DIMACS/AMS31 (1996), 149–184.

12.

Wang

, Zhang

, Gu

and Pung

H.K.

, Ontology Based Context Modeling and Reasoning using OWL, 2nd IEEE Conference on Pervasive Computing and Communications Workshops (PerCom),IEEE Computer Society (2004), pp. 18–22.