Topics in monitoring and planning for embedded real-time systems
<p>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.</p> <p>The...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | English |
| Published: |
2015
|
| Subjects: |
| _version_ | 1797104022527672320 |
|---|---|
| author | Ho, H |
| author2 | Ouaknine, J |
| author_facet | Ouaknine, J Ho, H |
| author_sort | Ho, H |
| collection | OXFORD |
| description | <p>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.</p> <p>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 <em>Metric Temporal Logic</em> (MTL) with two families of new modalities is expressively complete for the <em>Monadic First-Order Logic of Order and Metric</em> (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.</p> <p>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 <em>k</em> 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.</p> |
| first_indexed | 2024-03-07T06:28:08Z |
| format | Thesis |
| id | oxford-uuid:f507756d-8bdc-4b1f-8bbf-214c9997f9c5 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T06:28:08Z |
| publishDate | 2015 |
| record_format | dspace |
| spelling | oxford-uuid:f507756d-8bdc-4b1f-8bbf-214c9997f9c52022-03-27T12:24:12ZTopics in monitoring and planning for embedded real-time systemsThesishttp://purl.org/coar/resource_type/c_db06uuid:f507756d-8bdc-4b1f-8bbf-214c9997f9c5Applications and algorithmsComputer science (mathematics)Modal logicTheory and automated verificationEnglishOxford University Research Archive - Valet2015Ho, HOuaknine, J<p>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.</p> <p>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 <em>Metric Temporal Logic</em> (MTL) with two families of new modalities is expressively complete for the <em>Monadic First-Order Logic of Order and Metric</em> (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.</p> <p>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 <em>k</em> 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.</p> |
| spellingShingle | Applications and algorithms Computer science (mathematics) Modal logic Theory and automated verification Ho, H Topics in monitoring and planning for embedded real-time systems |
| title | Topics in monitoring and planning for embedded real-time systems |
| title_full | Topics in monitoring and planning for embedded real-time systems |
| title_fullStr | Topics in monitoring and planning for embedded real-time systems |
| title_full_unstemmed | Topics in monitoring and planning for embedded real-time systems |
| title_short | Topics in monitoring and planning for embedded real-time systems |
| title_sort | topics in monitoring and planning for embedded real time systems |
| topic | Applications and algorithms Computer science (mathematics) Modal logic Theory and automated verification |
| work_keys_str_mv | AT hoh topicsinmonitoringandplanningforembeddedrealtimesystems |