Abstract-Statistical Model Checking (SMC) är en beräkningsmässigt mycket effektiv verifieringsteknik baserad på selektiv systemprovtagning. En väl identifierad brist hos SMC är att den, till skillnad från probabilistisk modellkontroll, inte kan tillämpas på system med icke-determinism, såsom Markov Decision Processes (MDP). Vi tar itu med denna begränsning genom att utveckla en algoritm som löser icke-determinism probabilistically, och sedan använder flera rundor av provtagning och förstärkning Lära sig att på ett tydligt sätt förbättra upplösningar av icke-determinism när det gäller att uppfylla en gränsad Linjär Temporal Logic (BLTL) egendom. Vår algoritm reducerar därmed en MDP till en helt probabilistisk Markov-kedja där SMC kan användas för att ge en ungefärlig lösning på problemet med att kontrollera den probabilistiska BLTL-fastigheten. Vi integrerar vår algoritm i en parallellmodifiering av PRISM-simuleringsramen. Omfattande validering med både nya och PRISM-riktmärken visar att metoden skalas mycket väl i scenarier där symboliska algoritmer misslyckas med att göra det.
I en statistisk modell för kontroll av Markovs beslutsprocesser REF kan det därför vara lämpligt att utvidga vår logik med belönande operatörer.
Statistical Model Checking for Markov Decision Processes
{'venue': '2012 Ninth International Conference on Quantitative Evaluation of Systems', 'journal': '2012 Ninth International Conference on Quantitative Evaluation of Systems', 'mag_field_of_study': ['Computer Science']}