Voogd, Erik (2018) Verifying LTL Specifications for Discrete-Time Dynamical Systems. Bachelor's Thesis, Mathematics.
|
Text
main.pdf Download (391kB) | Preview |
|
![[img]](https://fse.studenttheses.ub.rug.nl/style/images/fileicons/text.png) |
Text
toestemming.pdf Restricted to Registered users only Download (98kB) |
Abstract
Linear-time temporal logic (LTL) is a class of logics whose formulas can express global, eventual, or repeated satisfaction of properties. We explore how to use LTL formulas for specifying properties of Discrete-time Dynamical Systems (DDS) on a continuous domain, and to verify them. To this end, a finite abstraction from the infinite system is constructed. The main result is that we can rigorously verify an LTL formula for a DDS using this abstraction and tools proposed in the literature.
| Item Type: | Thesis (Bachelor's Thesis) |
|---|---|
| Supervisor name: | Besselink, B. and Perez Parra, J.A. |
| Degree programme: | Mathematics |
| Thesis type: | Bachelor's Thesis |
| Language: | English |
| Date Deposited: | 19 Jul 2018 |
| Last Modified: | 26 Jul 2018 12:09 |
| URI: | https://fse.studenttheses.ub.rug.nl/id/eprint/17966 |
Actions (login required)
 |
View Item |