Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking
Created by
Haebom
Category
Empty
저자
Linus Heck, Filip Macak, Milan \v{C}e\v{s}ka, Sebastian Junges
개요
유한 마르코프 결정 과정(MDP)에 대한 보상 최적 정책을 계산하는 능력은 계획, 컨트롤러 합성, 검증 등 다양한 응용 분야의 기반이 됩니다. 이 논문은 MDP의 섭동에 강건하고 표현 또는 구현 비용과 관련된 추가적인 구조적 제약 조건을 만족하는 정책을 계산하는 접근 방식을 제시합니다. 유연성을 위해 MDP 집합에 대한 1차 논리 이론으로 제약 조건을 표현하며, 효율성을 위해 만족성 솔버와 확률적 모델 체킹 알고리즘을 긴밀하게 통합합니다.