2013/07/11 by Igor Cizelj, Cizelj, Igor, Călin Belta +1
Computer Science · Engineering · #Autonomous Vehicle Technology and Safety #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Robotics (cs.RO) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1307.3224
openalex publication_date 2013/07/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We propose a human-supervised control synthesis method for a stochastic\nDubins vehicle such that the probability of satisfying a specification given as\na formula in a fragment of Probabilistic Computational Tree Logic (PCTL) over a\nset of environmental properties is maximized. Under some mild assumptions, we\nconstruct a finite approximation for the motion of the vehicle in the form of a\ntree-structured Markov Decision Process (MDP). We introduce an efficient\nalgorithm, which exploits the tree structure of the MDP, for synthesizing a\ncontrol policy that maximizes the probability of satisfaction. For the proposed\nPCTL fragment, we define the specification update rules that guarantee the\nincrease (or decrease) of the satisfaction probability. We introduce an\nincremental algorithm for synthesizing an updated MDP control policy that\nreuses the initial solution. The initial specification can be updated, using\nthe rules, until the supervisor is satisfied with both the updated\nspecification and the corresponding satisfaction probability. We propose an\noffline and an online application of this method.\n