Show simple item record

dc.contributor.authorCizelj, Igoren_US
dc.date.accessioned2015-04-24T19:48:56Z
dc.date.available2015-04-24T19:48:56Z
dc.date.issued2014
dc.date.submitted2014
dc.identifier.other
dc.identifier.urihttps://hdl.handle.net/2144/10967
dc.descriptionThesis (Ph.D.)--Boston Universityen_US
dc.description.abstractTemporal logics, such as Linear Temporal Logic (LTL) and Computation Tree Logic (CTL), have become increasingly popular for specifying complex mission specifications in motion planning and control synthesis problems. This dissertation proposes and evaluates methods and algorithms for synthesizing control strategies for different vehicle models from temporal logic specifications. Complex vehicle models that involve systems of differential equations evolving over continuous domains are considered. The goal is to synthesize control strategies that maximize the probability that the behavior of the system, in the presence of sensing and actuation noise, satisfies a given temporal logic specification. The first part of this dissertation proposes an approach for designing a vehicle control strategy that maximizes the probability of accomplishing a motion specification given as a Probabilistic CTL (PCTL) formula. Two scenarios are examined. First, a threat-rich environment is considered when the motion of a vehicle in the environment is given as a finite transition system. Second, a noisy Dubins vehicle is considered. For both scenarios, the motion of the vehicle in the environment is modeled as a Markov Decision Process (MDP) and an approach for generating an optimal MDP control policy that maximizes the probability of satisfying the PCTL formula is introduced. The second part of this dissertation introduces a human-supervised control synthesis method for a noisy Dubins vehicle such that the expected time to satisfy a PCTL formula is minimized, while maintaining the satisfaction probability above a given probability threshold. A method for abstracting the motion of the vehicle in the environment in the form of an MDP is presented. An algorithm for synthesizing an optimal MDP control policy is proposed. If the probability threshold cannot be satisfied with the initial specification, the presented framework revises the specifica- tion until the supervisor is satisfied with the revised specification and the satisfaction probability is above the threshold. The third part of this dissertation focuses on the problem of stochastic control of a noisy differential drive mobile robot such that the probability of satisfying a time constrained specification, given as a Bounded LTL (BLTL) formula, is maximized. A method for mapping noisy sensor measurements to an MDP is introduced. Due to the size of the MDP, finding the exact solution is computationally too expensive. Correctness is traded for scalability, and an MDP control synthesis method based on Statistical Model Checking is introduced.en_US
dc.language.isoen_US
dc.publisherBoston Universityen_US
dc.titleVehicle control from temporal logic specifications with probabilistic satisfaction guaranteesen_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