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.

[img]
Preview
Text
main.pdf

Download (391kB) | Preview
[img] 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:
Supervisor nameSupervisor E mail
Besselink, B.B.Besselink@rug.nl
Perez Parra, J.A.J.A.Perez@rug.nl
Degree programme: Mathematics
Thesis type: Bachelor's Thesis
Language: English
Date Deposited: 19 Jul 2018
Last Modified: 26 Jul 2018 12:09
URI: http://fse.studenttheses.ub.rug.nl/id/eprint/17966

Actions (login required)

View Item View Item