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.
