2026-07-24T02:44:01Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5610 2024-03-06T10:29:42Z ddc:004 open_access

Parameter and Controller Synthesis for Markov Chains with Actions and State Labels Tati, Bharath Siva Kumar Siegle, Markus Markov chains with actions and state labels Parameter synthesis Controller synthesis Probabilistic model checking This paper introduces a novel approach for synthesizing parameters and controllers for Markov Chains with Actions and State Labels (ASMC). Requirements which are to be met by the controlled system are specified as formulas of asCSL, which is a powerful temporal logic for characterizing both state properties and action sequences of a labeled Markov chain. The paper proposes two separate - but related - algorithms for untimed until type and untimed general asCSL formulas. In the former case, a set of transition rates and a common rate reduction factor are determined. In the latter case, a controller which is to be composed in parallel with the given ASMC is synthesized. Both algorithms are based on some rather simple heuristics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Bharath Siva Kumar Tati and Markus Siegle 2015 Is Part Of OASIcs, Volume 44, 2nd International Workshop on Synthesis of Complex Parameters (SynCoP'15) (2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.SynCoP.2015.63 urn:nbn:de:0030-drops-56107 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SynCoP.2015.63 eng https://creativecommons.org/licenses/by/3.0/legalcode