Show simple item record

dc.contributor.authorGöl, Ebru Aydinen_US
dc.date.accessioned2015-04-24T19:41:41Z
dc.date.available2015-04-24T19:41:41Z
dc.date.issued2014
dc.date.submitted2014
dc.identifier.other
dc.identifier.urihttps://hdl.handle.net/2144/10934
dc.descriptionThesis (Ph.D.)--Boston Universityen_US
dc.description.abstractTemporal 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 affine 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 finite 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 affine 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.en_US
dc.language.isoen_US
dc.publisherBoston Universityen_US
dc.titleFormal verification and controller synthesis for discrete-time systemsen_US
dc.typeThesis/Dissertationen_US
etd.degree.nameDoctor of Philosophyen_US
etd.degree.leveldoctoralen_US
etd.degree.disciplineSystems Engineeringen_US
etd.degree.grantorBoston Universityen_US


This item appears in the following Collection(s)

Show simple item record