Model Checking Based Query and Retrieval in OpenStreetMap.

OpenStreetMap (OSM) is a crowd source geographical database that gives users a wide range of tools for searching and locating points of interest and to support the user in navigation on a map. This paper proposes to define a query language for OSM specifying user requests about the route to select between a source and a destination. To this purpose we use Uppaal (http://www.uppaal.org/) model checker: the user poses her query specifying desired points of interest via temporal logic. the method model checks the negation of the desired property, whose counterexample will retrieve the desired path.