2018/04/30 by Christel Baier, Nathalie Bertrand, Baier, Christel +7
Computer Science · #Formal Methods in Verification #Bayesian Modeling and Causal Inference #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1804.11301
The paper deals with finite-state Markov decision processes (MDPs) with\ninteger weights assigned to each state-action pair. New algorithms are\npresented to classify end components according to their limiting behavior with\nrespect to the accumulated weights. These algorithms are used to provide\nsolutions for two types of fundamental problems for integer-weighted MDPs.\nFirst, a polynomial-time algorithm for the classical stochastic shortest path\nproblem is presented, generalizing known results for special classes of\nweighted MDPs. Second, qualitative probability constraints for weight-bounded\n(repeated) reachability conditions are addressed. Among others, it is shown\nthat the problem to decide whether a disjunction of weight-bounded reachability\nconditions holds almost surely under some scheduler belongs to textrmNP\∩\n textrmcoNP, is solvable in pseudo-polynomial time and is at least as hard\nas solving two-player mean-payoff games, while the corresponding problem for\nuniversal quantification over schedulers is solvable in polynomial time.\n