Permissive Supervisor Synthesis for Markov Decision Processes Through Learning
From MaRDI portal
Publication:5228317
DOI10.1109/TAC.2018.2879505zbMATH Open1482.90241arXiv1703.07351OpenAlexW2964263874WikidataQ128911357 ScholiaQ128911357MaRDI QIDQ5228317FDOQ5228317
Hai Lin, Xiao-Bin Zhang, Bo Wu
Publication date: 12 August 2019
Published in: IEEE Transactions on Automatic Control (Search for Journal in Brave)
Abstract: This paper considers the permissive supervisor synthesis for probabilistic systems modeled as Markov Decision Processes (MDP). Such systems are prevalent in power grids, transportation networks, communication networks and robotics. Unlike centralized planning and optimization based planning, we propose a novel supervisor synthesis framework based on learning and compositional model checking to generate permissive local supervisors in a distributed manner. With the recent advance in assume-guarantee reasoning verification for probabilistic systems, building the composed system can be avoided to alleviate the state space explosion and our framework learn the supervisors iteratively based on the counterexamples from verification. Our approach is guaranteed to terminate in finite steps and to be correct.
Full work available at URL: https://arxiv.org/abs/1703.07351
Specification and verification (program logics, model checking, etc.) (68Q60) Markov and semi-Markov decision processes (90C40)
Cited In (1)
This page was built for publication: Permissive Supervisor Synthesis for Markov Decision Processes Through Learning
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5228317)
