Boston University Libraries OpenBU
    JavaScript is disabled for your browser. Some features of this site may not work without it.
    View Item 
    •   OpenBU
    • Theses & Dissertations
    • Boston University Theses & Dissertations
    • View Item
    •   OpenBU
    • Theses & Dissertations
    • Boston University Theses & Dissertations
    • View Item

    Vehicle control from temporal logic specifications with probabilistic satisfaction guarantees

    Thumbnail
    Date Issued
    2014
    Author(s)
    Cizelj, Igor
    Share to FacebookShare to TwitterShare by Email
    Export Citation
    Download to BibTex
    Download to EndNote/RefMan (RIS)
    Metadata
    Show full item record
    Permanent Link
    https://hdl.handle.net/2144/10967
    Abstract
    Temporal 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.
    Description
    Thesis (Ph.D.)--Boston University
    Collections
    • Boston University Theses & Dissertations [7778]


    Boston University
    Contact Us | Send Feedback | Help
     

     

    Browse

    All of OpenBUCommunities & CollectionsIssue DateAuthorsTitlesSubjectsThis CollectionIssue DateAuthorsTitlesSubjects

    Deposit Materials

    LoginNon-BU Registration

    Statistics

    Most Popular ItemsStatistics by CountryMost Popular Authors

    Boston University
    Contact Us | Send Feedback | Help