Master Thesis Proposals

Real-Time Characteristics of Data Management in an Autonomous UAV

1. Collect data about the actual performance and the actual demands on the data management in an autonomous UAV;
2. develop a characterization of the real-time data management issues; and
3. survey existing real-time data management systems to see if anything matches the requirements.

Similarity Metrics for Anchoring

Traffic Monitoring using Probabilistic Approaches

Partial Evaluation of Temporal Logics

1. Handle other logics (to include freeze quantification, until with two intervals, and so on) and larger fragments of TAL.
2. Instead of evaluating a single formula over a single trace evaluate a single formula on all suffixes of a trace (to find all positive instances of a formula and implicitly all false instances).
3. Do partial evaluation with sets of traces instead of a single trace. To progress sets of traces, is that the same as progressing branching time logics? Is there any difference between progression over sets of traces and normal model checking? If we have all the observations as either a timed automata or a temporal logical formula then it would be the same as model checking. The difference is that the set of formulas changes over time and the algorithm should make sure that the formula always can be evaluated to true. I think that this last extension actually is a generalization of the model checking problem where the instance checking problem is one extreme and the model checking problem is the other extreme (all the knowledge of this particular instance vs no knowledge about the particular instance). But the intentions might be different.
4. Combine a trace of observations and a model of the future behavior. The intension is then to monitor that there are at least some of the future behavior which will lead to the desired behavior. This would allow us to trigger an execution monitor much sooner since we can predict that the execution will fail. One, somewhat contrived, example would be the case where the agent enters a dead end while the formula only checks that the agent can move forward. These cases might all be possible to solve using more complex formulas. The interesting question is then whether it is easier to write these formulas than to provide a predictive model and evaluate the future traces. Since the evaluation most likely is very expensive (PSPACE or EXPSPACE) we probably only want to evaluate the future traces up to a certain temporal predictive horizon.

Another extension which doesn't have that much to do with progression is how to handle the first order extension of the propositional temporal logic. The main issue is how to handle objects which come and go. This is probably a trivial extension since there are basically two options (quantification is either done over all objects which always exists but whose existence can be modeled using a predicate or over only those objects that exists in the current state). The only "difficulty" with the second approach is that existence of objects might be retroactive. If the UAV finds a car at time-point t this means that the car most likely has existed at least for several months. The interpretation would then have to be changed to "those objects which are known to exist in the current state", which is a subject interpretation as a contrary to the objective where all objects always exists. Even if it is known that an object exists its features might not be known.

Another interesting avenue is to make not only the state sequence but also the states themselves incomplete. Instead of progressing a formula over a complete state we would progress a formula over a partial state which could very well be a single proposition or assignment of a feature. A fundamental requirement will most likely be that the stream of values for a single proposition/feature is ordered by valid time (i.e. if feature f has a value at t, then no new observations about its value at or before t will be made).

Yet another extension would be to add a theory for how to complete a partial state into either a complete state or a less partial state. An example could be that an operator has said that all cars in the area are of a certain type, for example Toyota since we are currently monitoring a Toyota factory. Then we could assume that the type of a car without an observation of the type is a Toyota. This ties into the whole area of default reasoning and what to do when an exception is detected. The nice thing with this would be that an operator can give general guidelines or advice which can be instantiated by the agent. Currently all observations must be fully instantiated.

One potential approach would be to translate the formula to a timed automata and then maintain a set of states where the evaluation is currently located. If all states are accepting states then the formula is evaluated to true, if no trace is a string in the language then the formula is evaluated to false. The interesting case is what to do with those traces that are not accepted by the language if there are other traces which are accepted. These could be used by the agent as input to an active sensing module which decides whether the agent should actually try to find out the actual value and to reduce the uncertainty.

Stream Generator Language/Testing Progression of Temporal Logical Formulas

Start from a timed automata (TA). Temporal logics can be translated to TAs. Extend the TA with a probability distribution for when the state will be left. This will not change the semantics of the TA but only change the distribution of traces generated by non-deterministic runs. It might be interesting to define a simpler stream language which can be translated to a TA.