1 Introduction

Open Street Map [11] is an initiative to create and provide free geographic data, such as street maps for the user who is looking for a path tailored to her needs. Anyway it is not always easy to detect an optimized route. For example the user locates her current position and searches on the map her destination, but along the path she needs to find some desired points of interest. Even though all the points of interest are easily localized on the map, a structured and automated search of them in the region of interest bounded by starting and arrival points is not available.

In this paper we introduce an approach to query OSM by specifying user’s requests with regard to the route to take between a source and a destination together with some potential point of interests. To this purpose the area of interest on the map is modeled in a graph containing the potential POIs for the user. The region of interest is extracted from the map and encoded in XML graph of the Uppall model checker’s syntax [2]. More precisely we model check the negation of the desired property, whose counterexample will retrieve the path satisfying the user’s needs. The main contributions are: (a) a translation of OSM map to UPPAAL; (b) a novel application of model checking technology; (c) temporal logic as a query languages on a map; (d) a monitoring automaton for temporal logics formulae verification. In the remaining of this paper we start by introducing some background notions on temporal logics and Uppaal Model checker in Sect. 2. We then propose our approach and describe the architecture of the developed system in Sect. 3. Conclusion and Future Work close the paper.

2 Background

Temporal Logics and Uppaal Model Checker. A Temporal Logic provides a formal system for reasoning about the truth values of assertions that change over time. In this section we briefly describe main categories of temporal logics The interested reader may refer to the surveys for temporal logics in [1, 4–6, 10].

Linear Temporal Logics (LTL). In a linear temporal logic the non-temporal portion of the logic is defined according to classical propositional logic. The formulae of LTL are built up from atomic propositions, truth-functional connectives (\(\vee , \wedge , \lnot \), etc.) and temporal operators. The basic temporal operators of this system are Fp (“sometime p” also read as “eventually p”), Gp (“always p” also read as “henceforth p”), Xp (“next time p”), and p U q (“p until q”). Branching Temporal Logics. A Branching Temporal Logic allows the use of basic temporal operators such as a path quantifier either A “for all futures” or E “for some future”, followed by a single one of the usual linear temporal operators G “always”, F “sometime”, X “next time”, or U “until”. Computation Tree Logic (CTL) is a Branching TL. Real time temporal logics. Real-time temporal logics are different in terms of expressiveness, order, time metric, temporal modalities, time model and time structure. They also have different capabilities for the specification and verification of real-time systems. TCTL is a real-time extension of CTL. It extends CTL with hidden clock bounded operators. UppaalFootnote 1 [2, 9, 12] is a toolbox for verification of real-time systems jointly developed by Uppsala University and Aalborg University. It has been applied successfully in several application problems ranging from communication protocols to multimedia applications. The tool is designed to verify systems that can be modelled as networks of timed automata extended with integer variables, structured data types, user defined functions, and channel synchronisation. Uppaal uses a simplified version of TCTL that consists of path formulae and state formulae. State formulae describe individual states and are expressions that can be evaluated for a state without looking at the behaviour of the model. Path formulae quantify over paths or traces of the model and can be classified into reachability, safety and liveness.

3 Approach

In this section we start by defining the mathematical model we use for managing the map in our method.

Definition 1

Region map. The region map is formally defined as a directed graph \(G=<N,E>\) that models the information about a geographical region. The nodes are point on the map that belong to the set \(N=\{n_0, n_1, ... n_n\}\); each \(n_i\) is a tuple \(n_i=(id, latitude, longitude)\); the edges belong to the set \(E=\{e_0, e_1, ... e_m\}\) where each \(e_j\) is a path between two nodes.

A subregion of the map is a subgraph \(S=<SN,SE>\) with \(SN \subseteq N\) and \(SE \subseteq E\) respectively.

The experimental framework we use adopts the Uppaal model checker and hence translates the region map in the XML-based internal encoding of the model checker.

Definition 2

Uppaal region map. A UPPAAL region map is a XML structure \(M=\{l\}\) where location l is the tuple \(l=(location, id, x, y, name)\).

With respect to other approaches, planning or other existing query languages [3, 7, 8], the approach we propose is strengthened by the use of TL and by the possibility to check the property expressed in TL. The choice of temporal logics was motivated by the possibility to give a sequence of points of interest or of events that the users desires to find. to check the property satisfaction we use model checking that gives the user as response the retrieved path if it exists. To retrieve the path the formula is negated and the path is obtained as counterexample of the property to verify.

The choice of Uppaal model checker was motivated by implementation issue concerned with its interface and data management. Even though Uppaal is mainly a Real-time system verifier it has been easily integrated in our approach to model a direct graph and to model a context in which systems are not necessarily time based, by using a monitoring automata. By the way, among other existing model checkers – Spin, NuSMv, Maude and so on – it proved several advantages as performance, usability, efficiency, and was really suitable for the purposes of our approach. Internal representation of data is instead supported by XML modeling thus enabling an easy reduction of OSM map to Uppaal model. At last with respect to other model checkers more obsolete and less flexible, Uppaal architectural model is much more open and interoperable to be integrated in even complex component based systems. Thanks to all these advantages we opted for using Uppaal instead of other model checkers and solved the well-known limitation in term of TL verification by using an ad hoc implemented module (the monitoring automata).

Monitoring Automaton. One of the main drawback of using Uppaal is the temporal logic verifier it embeds. In fact, it is able to check only a subset of the temporal logic without nested operator. The query: The user is leaving on the state START, she wants to reach the state END and wants to pass a POI before reaching her destination. is not directly executable with Uppaal because it is not possible to nest more than one temporal operator. To solve this drawback we use a Monitoring Automaton, i.e. an automaton whose state transition depends on the occurrence of properties in a secondary automaton. To make sure that required properties are verified on the primary automaton it is sufficient to check that the secondary automaton, the monitor, has reached a certain state. So it is sufficient to design the monitor automaton to move to a new state each time a specific condition changes and then formulate query on that automaton. The term monitoring automaton is derived from the presence of a robot that monitors that POI will be crossed.

3.1 Prototype System

The architectural framework of the navigation system we developed is made up of several integrated components:

  • A Graphical interface where the user poses her query through a simple selection of icons or points of interest.

  • Overpass turbo APIs for accessing and manipulating OSM data.

  • A XML parser for extracting and filtering data from OSM and to select intermediate points of the route.

  • The XML file extracted from the parser that models the Uppaal’s model checker graph.

  • A CTL/LTL package for modeling user’s query in temporal logics specifications.

  • A Monitoring Automaton (see below) used to verify some complex Temporal logics specifications with nested operators or quantifiers not directly verifiable by Uppaal verifier.

The Overpass APIFootnote 2 (or OSM3S) is a read-only API that serves up custom selected parts of the OSM map data. Unlike the main API, which is optimized for editing, Overpass API is optimized for data consumers that need a few elements selected by search criteria like e.g. location, type of objects, tag properties, proximity, or combinations of them.

In a typical scenario, the user selects a starting point on the map and a destination, specifying the characteristics of the path in terms of POIs. For example, if the user requires a place to sleep she will be looking for POIs classified as hotels, B&B, etc. If she requires a place to eat the categories of course include restaurant, pizzeria, snack bar. The graphical interface allows the user to enter the specifications using a text box or by selecting the icon of the required point of interest. The iconic or textual query formulated by the user is translated into a Temporal Logic formula and provided as input to the Uppaal verifier.

Fig. 1.
figure 1

An example of retrieved path

Full size image

To retrieve the path satisfying the user’s needs we model check the negation of the desired property, whose counterexample will give us the desired path. Let us now briefly consider some query examples in LTL that the user can pose to the framework. Suppose the user is unaware of the syntax of the logical language. The application scenario is the following: the user is in Bari in the University campus and starting from this point she wants to go downtown, specifically to have lunch. She also needs to find an ATM to withdraw some money. She is going by car so she wants to avoid pedestrian street and before arriving to the restaurant she wants to find a car parking. As a final remark, she also wants to avoid peripheral areas in order to have the opportunity to visit the city even while driving. The logical form of the query can be specified as follows using specification patterns as:

\(Between ((START) \wedge (END))\)

\(Absence ((Peripheral zones) \wedge (Pedestrian))\)

\(Existence ((ATM) \wedge (Parking) \wedge (Restaurant))\)

\(After(Parking)\ Existence(Restaurant)\)

Starting from Start to End, avoid pedestrian then look for ATM and after parking find restaurant that in LTL is formalized as:

\(({\texttt {G}}(START) \wedge {\texttt {G}}(\lnot (END) \wedge {\texttt {F}}(END)) \rightarrow ( \lnot ( (Pedestrain) \wedge (\lnot (Peripheral) \wedge {\texttt {F}}(ATM) \wedge (Parking) \wedge (Restaurant) ) \wedge ({\texttt {G}} \lnot (ATM) \vee ({\texttt {F}}(Restaurant) \wedge ({\texttt {F}}( Parking) \wedge {\texttt {F}}(Restaurant))))\)

Figure 1 shows the retrieved path after the query evaluation.

4 Conclusion and Future Work

In this paper we proposed a model-based approach to query Open Street Map. We used temporal logics to specify user’s requests about the map and Uppaal model checker, properly embedded in a Java navigation system, to check and verify the queries posed by the user. We modeled the area of interest on the map as a graph containing the potential POIs for the user and then we pose the query as a temporal logic formula thus allowing the system to solve the overall problem via model checking techniques. We are currently working to develop a Domain Specific Language to hide the LTL operators for normal users. At last, we are extending our proposal to build an app working in a mobile environment, to allow the user to get access to the map using his smartphone.