Parameter and controller synthesis for Markov chains with actions and state labels. (English) Zbl 1429.68142
André, Étienne (ed.) et al., 2nd international workshop on synthesis of complex parameters, SynCoP’15, April 11, 2015, London, UK. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. OASIcs – OpenAccess Ser. Inform. 44, 63-76 (2015).
Summary: 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 as CSL, 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 as CSL 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.
For the entire collection see [Zbl 1392.68009].
For the entire collection see [Zbl 1392.68009].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 60J20 | Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
Keywords:
Markov chains with actions and state labels; parameter synthesis; controller synthesis; probabilistic model checkingReferences:
| [1] | J. Bachmann, M. Riedl, J. Schuster, and M. Siegle. An efficient symbolic elimination algorithm for the stochastic process algebra tool CASPA. In 35th Int. Conf. on Current Trends in Theory and Practice of Computer Science (SOFSEM’09), pages 485-496. Springer LNCS 5404, 2009. · Zbl 1206.68208 |
| [2] | C. Baier, L. Cloth, B. Haverkort, M. Kuntz, and M. Siegle. Model checking Markov chains with Actions and State labels. IEEE Trans. on Software Engineering, 33(4):209-224, 2007. |
| [3] | C. Baier, B. Haverkort, H. Hermanns, and J.-P. Katoen. Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. on Software Engineering, 29(7), July 2003. · Zbl 0974.68017 |
| [4] | L. Brim, M. Češka, S. Dražan, and D. Šafránek. Exploring parameter space of stochastic biochemical systems using quantitative model checking. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, volume 8044 of LNCS, pages 107-123. Springer Berlin Heidelberg, 2013. |
| [5] | C. Daws. Symbolic and parametric model checking of discrete-time Markov chains. In Theor. Aspects of Computing - ICTAC 2004, volume 3407 of LNCS, pages 280-294. Springer Berlin Heidelberg, 2005. · Zbl 1108.68497 |
| [6] | E.M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. Param: A model checker for parametric Markov models. In Computer Aided Verification, volume 6174 of LNCS, pages 660-664. Springer Berlin Heidelberg, 2010. |
| [7] | E.M. Hahn, H. Hermanns, and L. Zhang. Probabilistic reachability for parametric Markov models. Int. Journal on Software Tools for Technology Transfer, 13(1):3-19, 2011. |
| [8] | T. Han, J.-P. Katoen, and A. Mereacre. Approximate parameter synthesis for probabilistic time-bounded reachability. In Real-Time Systems Symposium, pages 173-182. IEEE, 2008. |
| [9] | H. Hermanns, U. Herzog, and J.-P. Katoen. Process algebra for performance evaluation. Theoretical Computer Science, 274:43-87, 2002. · Zbl 0992.68149 |
| [10] | A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A tool for automatic verification of probabilistic systems. In Proc. 12th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’ 06), volume 3920 of LNCS, pages 441-444. Springer, 2006. |
| [11] | M. Kuntz and M. Siegle. Deriving symbolic representations from stochastic process algebras. In Process Algebra and Probabilistic Methods, Proc. PAPM-PROBMIV’02, pages 188-206. Springer, LNCS 2399, 2002. · Zbl 1065.68594 |
| [12] | M. Lawford and W.M. Wonham. Supervisory control of probabilistic discrete event systems. In Proc. of the 36th Midwestern Symposium on Circuits and Systems, 1993., pages 327-331, vol.1, 1993. |
| [13] | V. Pantelic, M. Lawford, and S. Postma. A framework for supervisory control of probabilistic discrete event systems. In 12th Int. Workshop on Discrete Event Systems (WODES 2014), pages 477-484, vol.12, 2014. · Zbl 1367.93371 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
