Formal verification and controller synthesis for discrete-time systems
Başlık çevirisi mevcut değil.
- Tez No: 402151
- Danışmanlar: PROF. CALIN BELTA
- Tez Türü: Doktora
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Bilim ve Teknoloji, Computer Engineering and Computer Science and Control, Science and Technology
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2014
- Dil: İngilizce
- Üniversite: Boston University
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Belirtilmemiş.
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 183
Özet
Özet yok.
Özet (Çeviri)
Temporal logics, such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL), are customarily used to specify the correctness of computer programs and digital circuits modeled as finite-state transition systems. In recent years, due to their expressivity and resemblance to natural language, temporal logics gained increasing popularity as specification languages for more realistic system models, such as dynamical systems. Most of the work approaching the problem of verifying and controlling non-trivial dynamical systems from rich specifications are centered on the concept of abstraction. This dissertation proposes theoretical frameworks and computational tools for the verification and control of continuous-state discrete-time systems from temporal logic specifications. The focus of this dissertation is on three particular classes of discrete-time systems, with widespread use in several areas: linear, switched linear, and piecewise afine systems. For switched linear systems, the existence of equivalent finite models is shown under stability constraints. Efficient algorithms to compute such finite models are developed. Moreover, algorithms for solving verification and synthesis problems from formulae of a particular fragment of LTL are designed, and are applied to equivalent fi- nite models of stable switched linear systems. For linear and piecewise affine systems, a novel language-guided procedure to design control strategies from temporal logic specifications is developed. The language-guided procedure combines the abstraction and temporal logic control of the finite model, and restricts the search for control strategies in such a way that the satisfaction of the specifications is guaranteed at all times. Furthermore, this procedure generates a characterization of all satisfying system trajectories in the form of sequences of polytopic sets, which allows synthesizing optimal control strategies from temporal logic specifications. In particular, a model predictive control (MPC) approach for optimal control of piecewise afine systems from temporal logic specifications is proposed. The MPC controller minimizes a cost over the trajectories of the system, while guaranteeing correctness with respect to a temporal logic formula. As an application, a computational framework for formal verification of synthetic gene networks from given experimental data is presented.
Benzer Tezler
- Anklaşman sistemi yazılım modelinin model sınamasının yapılması
Model verification of interlocking software model
DAVUT POLAT
Yüksek Lisans
Türkçe
2015
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrolİstanbul Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
YRD. DOÇ. DR. TOLGA OVATMAN
- Süperkavite su altı araçlarının hidrodinamik modellenmesi ve karakteristiğinin incelenmesi
Modelling and investigation of the hydrodynamic characteristics of supercavitating underwater vehicles
SEZER KEFELİ
Yüksek Lisans
Türkçe
2021
Deniz Bilimleriİstanbul Teknik ÜniversitesiUçak ve Uzay Mühendisliği Ana Bilim Dalı
PROF. DR. ELBRUS JAFAROV
- A small-format microbolometer imaging sensor with digital video outputs
Sayısal video çıkışlı ve küçük boyutlu mikrobolometre görüntüleme sensörü
CEM YALÇIN
Yüksek Lisans
İngilizce
2016
Elektrik ve Elektronik MühendisliğiOrta Doğu Teknik ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. TAYFUN AKIN
- K-TDA sözlük öğrenmesi ile görüntü zenginleştirerek iris tanıma
Iris recognition based on image enhancement using K-SVD dictionary learning
ALİ BİRCAN
Yüksek Lisans
Türkçe
2021
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolKonya Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
DR. ÖĞR. ÜYESİ NURDAN BAYKAN