Query Language for Location-Based Services: A Model Checking Approach

Christian HOAREAU  Ichiro SATOH  

IEICE TRANSACTIONS on Information and Systems   Vol.E91-D   No.4   pp.976-985
Publication Date: 2008/04/01
Online ISSN: 1745-1361
DOI: 10.1093/ietisy/e91-d.4.976
Print ISSN: 0916-8532
Type of Manuscript: Special Section PAPER (Special Section on Knowledge-Based Software Engineering)
Category: Ubiquitous Computing
ubiquitous computing,  location-based services,  query language,  model checking,  

Full Text: PDF(481.3KB)>>
Buy this Article

We present a model checking approach to the rationale, implementation, and applications of a query language for location-based services. Such query mechanisms are necessary so that users, objects, and/or services can effectively benefit from the location-awareness of their surrounding environment. The underlying data model is founded on a symbolic model of space organized in a tree structure. Once extended to a semantic model for modal logic, we regard location query processing as a model checking problem, and thus define location queries as hybrid logic-based formulas. Our approach is unique to existing research because it explores the connection between location models and query processing in ubiquitous computing systems, relies on a sound theoretical basis, and provides modal logic-based query mechanisms for expressive searches over a decentralized data structure. A prototype implementation is also presented and will be discussed.