Model Checking for Gaze Pattern Recognition

Automated gaze pattern recognition has found applications in several settings: software evaluation, marketing, education, etc. Traditional algorithms apply string matching approaches to obtain patterns from scanpaths (sequences of eye fixations). Although string matching algorithms have been widely studied and can be highly efficients, which is of crucial importance in real time applications, only relatively simple patterns can be recognized. In the current paper, we propose the use of linear temporal logic (LTL) as an expressive pattern specification language. Expressive patterns involving temporality and loops can be succinctly expressed. These expressive patterns are detected by a model checking algorithm for LTL. The algorithm decides if a formula satisfies or not a given model. In our proposal, the scanpath represents the model and the formula represents the pattern. We illustrate this proposal with some experiments.