Skip to Main content Skip to Navigation
Theses

Efficient verification of real time systems

Abstract : Timed automata are often used to model real-time systems. The reachability problem is of particular interest since it allows us to check for safety properties, but also build controllers for motion planning for example. Although this problem has been solved for 25 years, and implementation of these algorithms can be found in many tools, we propose some algorithms to speed up this process in particular cases. For safety problems, we propose and test abstraction based methods, that overestimate zones of a time space that could be reachable. These abstractions are then refined successively through a CEGAR loop. As for the problem of controller generation for motion planning, we propose algorithms based on heuristic search and A*. For all these algorithms we then show experimental results that we obtained with our implementation.
Complete list of metadatas

https://hal.archives-ouvertes.fr/tel-03121385
Contributor : Victor Roussanaly <>
Submitted on : Tuesday, January 26, 2021 - 1:11:26 PM
Last modification on : Thursday, January 28, 2021 - 3:11:51 AM

File

manuscritRoussanaly.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-03121385, version 1

Citation

Victor Roussanaly. Efficient verification of real time systems. Formal Languages and Automata Theory [cs.FL]. Université Rennes 1, 2020. English. ⟨tel-03121385⟩

Share

Metrics

Record views

42

Files downloads

30