Javascript must be enabled for the correct page display

Verifying LTL Specifications for Discrete-Time Dynamical Systems

Voogd, Erik (2018) Verifying LTL Specifications for Discrete-Time Dynamical Systems. Bachelor's Thesis, Mathematics.


Download (391kB) | Preview
[img] Text
Restricted to Registered users only

Download (98kB)


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

Actions (login required)

View Item View Item