Consistency checking of attention aware systems

Abstract

Attention aware systems keep track of users attention in order to react and provide a better interaction experience. In the educational setting, recent research results have showed attention aware system can be useful in many smart learning scenarios, such as in student performance evaluation, and identi cation and motivation of inattentive students. However, ensuring a consistent behavior in these systems have been found a challenging task. This is due to the rich and heterogeneous contexts required to be modeled. Formal veri cation methods for these systems is then a demanding incipient research perspective. In the current work, we study a formal notion of consistency in attention aware systems for the educational setting. An expressive modal logic is proposed as speci cation language, and a consistency checking algorithm is provided. The algorithm is de ned in terms of the satis ability problem of the logic.

Keywords

• Formal Veri cation
• Attention Aware Systems
• Modal Logics

Introduction

Consider the following scenario in a smart learning environment, say a classroom. One or several instructors are helping to a number of students to carry out a learning activity (which can be divided in sub-activities). For this purpose, instructor(s) and students have access to a number of smart devices: interactive board, computers, phones, etc. At some point during the learning activity, students are supposed to solve some mathematical problems. One of these students seems frustrated when trying to solve these problems. Frustration may be detected by facial expression or gaze patterns [ 12 ]. Once this inattentive state (frustration) is detected by the smart classroom system, a tutorial video on how to solve the mathematical problems pops-up on the student's screen. An student with a di erent learning style may obtain a text lesson on related problems instead of the tutorial video. If after some time, the student still seem frustrated, Copyright © 2019 for this paper by its authors. one of the instructors, the mathematician, receives a corresponding alert in his mobile phone, in order to not disturb other students. This is a traditioAntatrlibsumtiaornt4.0 International (CC BY 4.0) learning environment scenario focused in the high engagement key feature de ning smart learning, according to [ 5 ]. Systems focused in this particular feature are also often called attention aware systems [ 11 ]. Systems capable to realize human perceptual and cognitives abilities, and to react in order to provide a better interaction experience.

Due to the rich and heterogeneous context in attention aware systems. The design process have become a very challenging task. This is because ensuring a consistent system behavior is such a vast context scales far beyond the developer scope. In this paper, we propose a formal notion of consistency in attention aware systems. This notion is de ned in terms of the satis ability of an expressive modal logic. This result implies a consistency checking algorithm. 1.1

Related Work

Due to the relatively recent introduction of studies on attention aware system [ 11 ], research on formal veri cation methods for these type of systems is basically incipient. Attention aware systems can also be seen a sort of contextaware system [ 3 ], where the context is focused on human attention aspects. Formal veri cation methods on context-aware systems have been studied in many settings [ 10 ], including the educational one [ 1 ].

In the setting of formal veri cation of context-aware systems, closest studies to our proposal are reported in [ 8,9 ]. In [ 8 ], formal veri cation of context-aware systems is de ned in terms of the satis ability of -calculus formulas. The calculus is an expressive modal logic with xed-point operators. In our proposal, we also verify system consistency of in terms of the satis ability of -calculus formulas. In contrast with context-aware systems veri ed in [ 8 ], veri cation of attention aware systems require the construction of deeper models. In [ 9 ], it is proposed a modeling and veri cation framework for context-aware systems in terms of consistency of knowledge bases of an expressive description logic. 1.2

Outline

In Section 2, we introduce the formal notions required to model and verify attention aware systems. In particular, since the notion of consistency is de ned in terms of tree-shaped models, we rst de ne tree-shaped Kripke structures. We also de ne in this section -calculus formulas, which are also interpreted in terms of Kripke structures. In Section 3, we rst de ne attention aware systems. In particular, inspired from [ 6 ], we de ne an attention aware smart learning environment. A formal notion of consistency of the environment is also introduced in this section. Section 4 is devoted to the description of a consistency checking algorithm for the attention aware smart learning environment. Consistency is described in terms of a -calculus formula. Additionally, we also show how to express temporal constraints on consistency models, such as restrictions on consecutive system interventions. Finally, in Section 5, we give a brief summary of our proposal. Further research perspective are also discussed in this last section.

Preliminaries

We introduce in this Section the speci cation language, the alternation-free propositional modal -calculus with converse. This is an expressive modal logic with a least and a greatest xed-points and converse modalities [ 4 ]. Since the notion of consistency of context-aware systems is de ned in terms of tree-shaped models [ 8 ], we then also interpret the speci cation language on tree structures. Before giving a precise notion of trees, we rst assume an alphabet composed by a countable set of proposition P , set of modalities M = f1; 2; 3; 4g, and a countable set of variables X.

A tree structure K is a tuple (N; R; L), where: { the set of nodes N is de ned as a complete pre x-closed non-empty nite set of words over the natural numbers N, that is, N is a nite set of words N N?, such that if n i 2 N , where n 2 N? and i 2 N, then also n 2 N ; { R : N M N is a transition relation, written n 2 R(n0; m), such that for all (n i); (n i + 1) 2 N , where i 2 N, n 2 R(n i; 1), (n i) 2 R(n; 3), (n i + 1) 2 R(n i; 2) and (n i) 2 R(n i + 1; 4), we say n is the parent of n i, hence n i is the child of n, n i + 1 is a following (right) sibling of n i, and hence n i is a previous (left) sibling of n i + 1; and { L : N 7! P is a total labeling function.

The speci cation language is now introduced. The set of -calculus formulas is de ned by the following grammar: ::= p j X j : j _ j hmi j

X: where p is a proposition, m a modalities, and X a variable.

Formulas are interpreted with respect to a tree structure K = (N; R; L) and a valuation function V : X 7! 2N , as follows. [[p]]VK = fn j L(n) = pg [[: ]]VK = N n [[ ]]VK [[hmi ]]VK = nn j R(n; m) \ [[ ]]VK 6= ; o [[X]]VK = V (X) [[ _ ]]VK = [[ ]]VK [ [[ ]]VK [[ X: ]]VK = \ nN 0 [[ ]]VK[N0 =X ]

N 0 o If there is a tree K such that the interpretation of a formula is not empty with respect to any valuation, then we say is satis able and K is a model of .

Intuitively, formulas are interpreted as follows. Propositions as node labels. Negations and disjunctions as set complements and unions, respectively. Modal formulas hmi as nodes can access through m to the interpretation of , that is, node(s) are children, parent, right and left sibling of h1i , h3i , h2i and h3i nodes, respectively. Fixed points can be seen as recursion operators, for instance, h1i X:p _ h1i X holds at nodes with at least one descendant named p.

Attention aware systems

We now introduce the notion of consistency in attention aware systems. For this, we rst de ne an attention aware system in the education setting inspired from [ 6 ]. The system is intended to engage inattentive students participating in a learning activity. Learning activities are carried on in a smart classroom equipped with sensors able to detect when students are not engaged in the activities. This disengagement embraces several scenarios, for instance when an student is inattentive or may be experiencing frustration because of the activity. According to the scenario, the system is supposed to react accordingly. For example, if the student is inattentive watching his mobile phone, the system may send a visual or sound alert directly to the student phone. In case the student is frustrated trying to solve some mathematical problems, the system may show in the student's screen a recall of the information associated to the problem is trying to solve. For this re-engagement process, the system must consider a huge legion of context constraints, such as the student learning style, the type of learning activity, the available devices, and so on. Intuitively, the notion of consistency for these systems aims to guarantee, at system design time, context constraints are satis ed. A consistent system must guarantee it is able to intervene in any possible disengagement scenario. In addition to the attention aware system proposed in [ 6 ], we also consider temporal and location constraints. These constraint types consider the consecutive repetition of system interventions on the same student in the same activity. Repeated system interventions may thus not impact in the engagement process as desired.

We then formally de ne an attention aware system by its input. The system input is de ned as a tuple (Sch; IL; IA; ID; SD; LD), where: { the schedule Sch is a set of tuples (t; l; la; s) associating times t, locations l, learning activities la, and students; { IL is composed by pairs (i; la) of interventions i and learning activities la; { IA is a set of pairs (i; a) of interventions i and attention states a; { (i; d) 2 ID relates interventions i with devices d; { (s; d) 2 SD denotes which devices d are accessible for each student s; and { (l; d) 2 LD indicates which devices d are available at each location l. Example 1. Consider for instance the following scenario, at 2 locations, 4 students (2 at each location) are participating in 2 activities at 2 time lapses. There are 2 types of attention states, say being inattentive and being frustrated. There are also 2 types of devices only: mobile phone and computer. The system can react in two di erent ways in order to attract the student attention, by a sound alert and by recalling a learned lesson. All these variables are related in several

: : : : : :

: : : : : : ak4 . . .

sk3 . . .

lk2 . . .

tk1 . . .

Times Locations Students Attention states Device

Intervention

It is not hard to see the system de ned in Example 1 is consistent because it is able to react in any possible scenario. Before giving a precise de nition of system consistency, we de ne a semantic notion of consistency in terms of a tree-shaped structure.

De nition 1 (Consistency model). Given a system input (Sch, IL, IA, ID, SD, LD), we de ne a tree structure (N; R; L), called the consistency model CM , as follows: { there is root node labeled by r; { for each time t occurring in Sch, the root has a child node labeled by the time proposition; { for each tuple (t; l; la; s) 2 Sch, the node labeled by t has a child labeled by l; { for each tuple (t; l; la; s) 2 Sch, the node labeled by l has a child labeled by s; { for each student in Sch, each student node has as many children as attention states occurring in IA; { each attention state node has at least one child node, labeled by a device d, such that (s; d) 2 SD, (l; d) 2 LD, and s and l label some ancestor nodes; and { each device node d has at least one child node, labeled by an intervention i, such that (i; d) 2 ID.

A canonic graphic representation of a consistency model is depicted in Figure 1.

Time constraints may help to increase the intervention e ect, that is, repeating an intervention at two consecutive times may not have the desired impact. In this work, time constraints where interventions cannot repeat at consecutive times are considered in addition. We then now give a precise notion of a consistent attention aware system.

De nition 2 (System consistency). Given a system input, we say the system is consistent, if and only if, there is a consistency model satisfying the time constraints. 4

Consistency checking

In this Section, we describe a consistency checking algorithm in terms of the satis ability of -calculus formula. We rst de ne a formula corresponding to a consistency model.

Given a system input (Sch; IL; IA; ID; SD; LD), we de ne the consistency formula as follows: j=2 k1 N1 :=h1i(t1 ^ N2(t1) ^ ^ h2ij 1(tj ^ N2(tj )) ^ h2ik1 1:h2i>)

k2(t) N2(t) :=h1i(l1 ^ la1 ^ N3(t; l1; la1) ^ ^ h2ij 1(lj ^ N3(t; lj ; laj ))^ h2ik2 1:h2i>) h2ik3 1:h2i>) N3(t; l; la) :=h1i(s1 ^ N4(t; l; la; s1) ^ 2 j 1(sj ^ N4(t; l; la; sj ))^ h i k4 N4(t; l; la; st) :=h1i(a1 ^ N5(t; l; la; s; a1) ^ ^ h2ij 1(aj ^ N5(t; l; la; s; aj ))^ h2ik4 1:h2i>) N5(t; l; la; s; a) :=(FDS (t; l; la; s; a) _ FLD(t; l; la; s; a)) ^ :h2i> where N6(t; l; la; s; a; d) :=

h1iij ^ :h2i> j=1 k6(la;a;d) _ j=1 provided that k1 is the number of time propositions in Sch, k2(t) is the number of locations, k3(t; l; la) is the number of students in the learning activity la, at location l, in time t, k4 is the number of attention states, kSD(s) is the number of devices available for student s, kLD(l) is the number of devices available at location l, and k6(la; a; d) is the number of interventions available for device d, learning activity a and attention state a.

As an example, consider the consistency model corresponding to the input system described in Example 1. The rst level of the model in the one for time lapses, N1 is then de ned as follows.

N1 :=h1i(t1 ^ N2(t1) ^ h2i(t2 ^ N2(t2)) ^ h2i:h2i>)

The second model level distinguishes the learning activities, there are two per time lapse.

N2(t1) :=h1i((la1 ^ l1) ^ N3(t1; la1; l1) ^ h2i((la2 ^ l2) ^ N3(t1; l2; la2))^ h2i:h2i>) N2(t2) :=h1i((la3 ^ l1) ^ N3(t2; la3; l1) ^ h2i((la4 ^ l2) ^ N3(t2; la4; l2))^ h2i:h2i>) The following level corresponds to the students. There are four students distributed in the two locations.

N3(t1; la1; l1) :=h1i(s1 ^ N4(t1; la1; l1; s1) ^ h2i(s2 ^ N4(t1; la1; l1; s2))^ h2i:h2i>) N3(t1; la2; l2) :=h1i(s3 ^ N4(t1; la2; l2; s3) ^ h2i(s4 ^ N4(t1; la2; l2; s4))^ h2i:h2i>) N3(t2; la3; l1) :=h1i(s1 ^ N4(t2; la3; l1; s1) ^ h2i(s2 ^ N4(t2; la3; l1; s2))^ h2i:h2i>) N3(t2; la4; l2) :=h1i(s3 ^ N4(t2; la4; l2; s3) ^ h2i(s4 ^ N4(t2; la4; l2; s4))^ h2i:h2i>)

In the fourth level, we must consider all possible scenarios of the attention states of each student at each location and time lapse.

N4(t1; la1; l1; s1) :=h1i(a1 ^ N5(t1; la1; l1; s1; a1) ^ h2i(a2 ^ N5(t1; la1; l1; s1; a2))

Level 5 constrains the availability of devices where the system engagement intervention is carried on. Location, student, and attention state constraints must be considered.

N5(t1; la1; l1; s1; a1) :=h1i(d1 ^ N6(t1; la1; l1; s1; a1; d1) ^ :h2i>) N5(t1; la1; l1; s1; a2) :=h1i(d2 ^ N6(t1; la1; l1; s1; a2; d2) ^ :h2i>) N5(t1; la1; l1; s2; a1) :=h1i(d1 ^ N6(t1; la1; l1; s2; a1; d1) ^ :h2i>) N5(t1; la1; l1; s2; a2) :=h1i(d2 ^ N6(t1; la1; l1; s2; a2; d2) ^ :h2i>) N5(t1; la2; l2; s3; a1) :=h1i(d1 ^ N6(t1; la3; l2; s3; a1; d1) ^ :h2i>) N5(t1; la2; l2; s3; a2) :=h1i(d2 ^ N6(t1; la3; l2; s3; a2; d2) ^ :h2i>) N5(t1; la2; l2; s4; a1) :=h1i(d1 ^ N6(t1; la2; l2; s4; a1; d1) ^ :h2i>) N5(t1; la2; l2; s4; a2) :=h1i(d2 ^ N6(t1; la2; l2; s4; a2; d2) ^ :h2i>) N5(t2; la3; l1; s1; a1) :=h1i(d1 ^ N6(t2; la3; l1; s1; a1; d1) ^ :h2i>) N5(t2; la3; l1; s1; a2) :=h1i(d2 ^ N6(t2; la3; l1; s1; a2; d2) ^ :h2i>) N5(t2; la3; l1; s2; a1) :=h1i(d1 ^ N6(t2; la3; l1; s2; a1; d1) ^ :h2i>) N5(t2; la3; l1; s2; a2) :=h1i(d2 ^ N6(t2; la3; l1; s2; a2; d2) ^ :h2i>) N5(t2; la4; l2; s3; a1) :=h1i(d1 ^ N6(t2; la4; l2; s3; a1; d1) ^ :h2i>) N5(t2; la4; l2; s3; a2) :=h1i(d2 ^ N6(t2; la4; l2; s3; a2; d2) ^ :h2i>) N5(t2; la4; l2; s4; a1) :=h1i(d1 ^ N6(t2; la4; l2; s4; a1; d1) ^ :h2i>) N5(t2; la4; l2; s4; a2) :=h1i(d2 ^ N6(t2; la4; l2; s4; a2; d2) ^ :h2i>)

The last level of the model corresponds to the system intervention available at each student disengagement scenario.

N6(t1; la1; l1; s1; a1; d1) :=h1i(i1 ^ :h2i>) N6(t1; la1; l1; s1; a2; d2) :=h1i(i2 ^ :h2i>) N6(t1; la1; l1; s2; a1; d1) :=h1i(i1 ^ :h2i>) N6(t1; la1; l1; s2; a2; d2) :=h1i(i2 ^ :h2i>) N6(t1; la2; l2; s3; a1; d1) :=h1i(i3 ^ :h2i>) N6(t1; la2; l2; s3; a2; d2) :=h1i(i3 ^ :h2i>) N6(t1; la2; l2; s4; a1; d1) :=h1i(i4 ^ :h2i>) N6(t1; la2; l2; s4; a2; d2) :=h1i(i4 ^ :h2i>) N6(t2; la3; l1; s1; a1; d1) :=h1i(i5 ^ :h2i>) N6(t2; la3; l1; s1; a2; d2) :=h1i(i5 ^ :h2i>) N6(t2; la3; l1; s2; a1; d1) :=h1i(i5 ^ :h2i>) N6(t2; la3; l1; s2; a2; d2) :=h1i(i5 ^ :h2i>) N6(t2; la4; l2; s3; a1; d1) :=h1i(i6 ^ :h2i>) N6(t2; la4; l2; s3; a2; d2) :=h1i(i6 ^ :h2i>) N6(t2; la4; l2; s4; a1; d1) :=h1i(i6 ^ :h2i>)

N6(t2; la4; l2; s4; a2; d2) :=h1i(i6 ^ :h2i>)

Time constraints consist in forbidding the occurrence of a system engagement intervention in consecutive time lapses. This can be modeled with a xed point operators. More precisely, given a system input (Sch; IL; IA; ID; SD; LD), we de ned the time constraints formula as follows:

k3 k6 NRT :=h1i T:(( ^ _ :FL(ij; sh) _ h2i:FL(ij; sh) ^ h2iT ) _ : h2i >) h=1 j=1 FL(i; s) :=h1i L:(FS(i; s) _ h2iL) FS(i; s) :=h1i S:((s ^ FA(i)) _ h2iS)

FA(i) :=h1i A:((h1iFD(i)) _ h2i A)

FD(i) :=h1ii where k3 is the number of students and k6 is the number of interventions.

Considering again the consistency model corresponding to the system de ned in Example 1. We then de ne the time constraints formula as follows: NRT :=h1i T:((FST1 ^ FST2 ^ FST3 ^ FST4 _ h2iT ) _ :h2i>) where

FST1 :=(:FL(i1; s1) _ h2i:FL(i1; s1)) ^ (:FL(i2; s1) _ h2i:FL(i2; s1))^ (:FL(i3; s1) _ h2i:FL(i3; s1)) ^ (:FL(i4; s1) _ h2i:FL(i4; s1))^ (:FL(i5; s1) _ h2i:FL(i5; s1)) ^ (:FL(i6; s1) _ h2i:FL(i6; s1)) FST2 :=(:FL(i1; s2) _ h2i:FL(i1; s2)) ^ (:FL(i2; s2) _ h2i:FL(i2; s2))^ (:FL(i3; s2) _ h2i:FL(i3; s2)) ^ (:FL(i4; s2) _ h2i:FL(i4; s2))^ (:FL(i5; s2) _ h2i:FL(i5; s2)) ^ (:FL(i6; s2) _ h2i:FL(i6; s2)) FST3 :=(:FL(i1; s3) _ h2i:FL(i1; s3)) ^ (:FL(i2; s3) _ h2i:FL(i2; s3))^ (:FL(i3; s3) _ h2i:FL(i3; s3)) ^ (:FL(i4; s3) _ h2i:FL(i4; s3))^ (:FL(i5; s3) _ h2i:FL(i5; s3)) ^ (:FL(i6; s3) _ h2i:FL(i6; s3)) FST4 :=(:FL(i1; s4) _ h2i:FL(i1; s4)) ^ (:FL(i2; s4) _ h2i:FL(i2; s4))^ (:FL(i3; s4) _ h2i:FL(i3; s4)) ^ (:FL(i4; s4) _ h2i:FL(i4; s4))^ (:FL(i5; s4) _ h2i:FL(i5; s4)) ^ (:FL(i6; s4) _ h2i:FL(i6; s4))

The main result of this work is then the correspondence of the existence of a tree-shaped model for the the consistency and time constraints -calculus formulas, and the consistency of attention aware systems.

Theorem 1. Given a system input (Sch; IL; IA; ID; SD; LD), the system is consistent, if and only if, [[N1 ^ NRT ]]VCM 6= ;, for any valuation V . Furthermore, deciding system consistency is in EXPTIME.

The proof goes by induction on the size of the system. From earlier complexity results [ 4,8 ], we can in addition characterize the complexity of this consistency problem. 5

Conclusions

In this paper, we described a consistency checking algorithm for attention aware systems. These systems are required to realize human perceptual and cognitives abilities, and to react in order to provide a better interaction experience. A consistency behavior of these systems implies the system is capable to react as it is supposed to, in any possible context scenario. We formalized this notion of consistency in terms of the satis ability of a -calculus formula. There is a model satisfying the formula, if and only if, the attention aware system is consistent. According to the known complexity of -calculus satis ability and the succinct encoding of system consistency provided in this paper, we also conclude the consistency problem of attention aware systems is en EXPTIME. Currently, we are developing -calculus satis ability algorithms as in [ 7 ], in order to provide practical consistency checking algorithms for attention aware systems. We are also interested in extensions of the -calculus, as with arithmetic operators [ 2 ], in order to model more complex constraints in attention aware systems.

References

1. Aguilar , J. , Jerez , M. , Rodr guez, T.: Cameonto: Context awareness meta ontology modeling . Applied Computing and Informatics 14 ( 2 ), 202 { 213 ( 2018 )

2. Barcenas , E. , Ben tez-Guerrero, E. , Lavalle , J.: On the model checking of the graded -calculus on trees . In: Sidorov, G. , Galicia-Haro , S.N . (eds.) Advances in Arti cial Intelligence and Soft Computing - 14th Mexican International Conference on Arti cial Intelligence , MICAI. Lecture Notes in Computer Science , vol. 9413 , pp. 178 { 189 . Springer ( 2015 )

3. Bettini , C. , Brdiczka , O. , Henricksen , K. , Indulska , J. , Nicklas , D. , Ranganathan , A. , Riboni , D.: A survey of context modelling and reasoning techniques . Pervasive and Mobile Computing 6 ( 2 ), 161 { 180 ( 2010 )

4. Bonatti , P.A. , Lutz , C. , Murano , A. , Vardi , M.Y.: The complexity of enriched mu-calculi . Logical Methods in Computer Science 4 ( 3 ) ( 2008 )

5. Gros , B. : The design of smart educational environments . Smart Learn. Environ . 3 ( 1 ), 15 ( 2016 )

6. Korozi , M. , Leonidis , A. , Antona , M. , Stephanidis , C. : LECTOR: towards reengaging students in the educational process inside smart classrooms . In: Horain, P. , Achard , C. , Mallem , M. (eds.) Intelligent Human Computer Interaction - 9th International Conference, IHCI, Proceedings. Lecture Notes in Computer Science , vol. 10688 , pp. 137 { 149 . Springer ( 2017 )

7. Limon , Y. , Barcenas , E. , Ben tez-Guerrero, E. , Medina , M.A. : Depth- rst reasoning on trees . Computacion y Sistemas 22 ( 1 ) ( 2018 )

8. Limon , Y. , Barcenas , E. , Ben tez-Guerrero, E. , Molero , G.: On the consistency of context-aware systems . Journal of Intelligent and Fuzzy Systems 34 ( 5 ), 3373 { 3383 ( 2018 )

9. Ram rez-Rueda, R. , Barcenas , E. , Mezura-Godoy , C. , Molero-Castillo , G. : Expressive context modeling with description logics . In: Villazon-Terrazas , B. , HidalgoDelgado , Y. (eds.) Knowledge Graphs and Semantic Web - First Iberoamerican Conference, KGSWC. Communications in Computer and Information Science , vol. 1029 , pp. 174 { 185 . Springer ( 2019 )

10. Riboni , D. , Bettini , C. : OWL 2 modeling and reasoning with complex human activities . Pervasive and Mobile Computing 7 ( 3 ), 379 { 395 ( 2011 )

11. Roda , C. , Thomas , J. : Attention aware systems: Theories, applications , and research agenda. Computers in Human Behavior 22 ( 4 ), 557 { 587 ( 2006 )

12. Rodriguez , A. , Barcenas , E. , Molero-Castillo , G. : Model checking for gaze pattern recognition . In: International Conference on Electronics, Communications and Computers , CONIELECOMP. pp. 170 { 175 . IEEE ( 2019 )