2017/06/20 by Christel Baier, Baier, Christel, Clemens Dubslaff +7
Biochemistry, Genetics and Molecular Biology · Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Gene Regulatory Network Analysis #Logic in Computer Science (cs.LO) #Performance (cs.PF) #Petri Nets in System Modeling
paper · pdf · doi:10.48550/arxiv.1706.06486
openalex publication_date 2017/06/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Continuous-time Markov chains with alarms (ACTMCs) allow for alarm events\nthat can be non-exponentially distributed. Within parametric ACTMCs, the\nparameters of alarm-event distributions are not given explicitly and can be\nsubject of parameter synthesis. An algorithm solving the \ε-optimal\nparameter synthesis problem for parametric ACTMCs with long-run average\noptimization objectives is presented. Our approach is based on reduction of the\nproblem to finding long-run average optimal strategies in semi-Markov decision\nprocesses (semi-MDPs) and sufficient discretization of parameter (i.e., action)\nspace. Since the set of actions in the discretized semi-MDP can be very large,\na straightforward approach based on explicit action-space construction fails to\nsolve even simple instances of the problem. The presented algorithm uses an\nenhanced policy iteration on symbolic representations of the action space. The\nsoundness of the algorithm is established for parametric ACTMCs with\nalarm-event distributions satisfying four mild assumptions that are shown to\nhold for uniform, Dirac and Weibull distributions in particular, but are\nsatisfied for many other distributions as well. An experimental implementation\nshows that the symbolic technique substantially improves the efficiency of the\nsynthesis algorithm and allows to solve instances of realistic size.\n