Topics in monitoring and planning for embedded real-time systems

Thesis

The verification of real-time systems has gained much interest in the formal verification community during the past two decades. In this thesis, we investigate two real-time verification problems that benefit from the techniques normally used in untimed verification.

The first part of this thesis is concerned with the monitoring of real-time specifications. We study the expressiveness of metric temporal logics over timed words, a problem that dates back to early 1990s. We show that the logic obtained by extending Metric Temporal Logic (MTL) with two families of new modalities is expressively complete for the Monadic First-Order Logic of Order and Metric (FO[<,+1]) in time-bounded settings. Furthermore, by allowing rational constants, expressive completeness also holds in the general (time-unbounded) setting. Finally, we incorporate several notions and techniques from LTL monitoring to obtain the first trace-length independent monitoring procedure for this logic.

The second part of this thesis concerns a decision problem regarding UAVs: given a set of targets (each ascribed with a relative deadline) and flight times between each pair of targets, is there a way to coordinate a flock of k identical UAVs so that all targets are visited infinitely often and no target is ever left unvisited for a time longer than its relative deadline? We show that the problem is PSPACE-complete even in the single-UAV case, thereby corrects an erroneous claim from the literature. We then complement this result by proposing an efficient antichain-based approach where a delayed simulation is used to prune the state space. Experimental results clearly demonstrate the effectiveness of our approach.

Authors: Ho, H

• Publication date: 2015
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: Oxford University, UK
• Language: English
• Keywords: antichains; real-time logics; monitoring; computational complexity; expressiveness; UAV
• Subjects: Applications and algorithms; Computer science (mathematics); Modal logic; Theory and automated verification