×

zbMATH — the first resource for mathematics

Constraint Markov chains. (English) Zbl 1223.68070
The article introduces constraint Markov chains as a new tool for specification. They are a generalization of interval Markov chains. Interval Markov chains extend Markov chains by labeling transitions with intervals, implying that each transition probability needs to be within the according interval. In constraint Markov chains these intervals are replaced by arbitrary constraints. This increases flexibility at the cost of increased complexity.
The authors discuss operations on such constraint Markov chains including refinement, parallel composition, conjunction, and tests for consistency and satisfaction. They provide clear and proven statements concentrating on closure properties and complexity of algorithms for these operations. While interval Markov chains are not even closed under conjunction, constraint Markov chains with linear constraints are. Moreover, constraint Markov chains with polynomial constraints are proven be to sufficient for closure for conjunction and parallel composition. Special cases like deterministic constraint Markov chains and connections to probabilistic automata are discussed.
The article is to a large degree self-contained. The presentation is clear and precise. Many small examples make the material accessible.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
60J10 Markov chains (discrete-time Markov processes on discrete state spaces)
Software:
CEGAR; SYNRAC
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Henzinger, T.A.; Sifakis, J., The embedded systems design challenge, (), 1-15
[2] Larsen, K.G., Modal specifications, (), 232-246
[3] Larsen, K. G.; Nyman, U.; Wąsowski, A., On modal refinement and consistency, (), 105-119 · Zbl 1151.68541
[4] Raclet, J.-B.; Badouel, E.; Benveniste, A.; Caillaud, B.; Legay, A.; Passerone, R., Modal interfaces: unifying interface automata and modal specifications, (), 87-96
[5] Larsen, K.G.; Nyman, U.; Wąsowski, A., Modal I/O automata for interface and product line theories, (), 64-79 · Zbl 1187.68296
[6] de Alfaro, L.; Henzinger, T.A., Interface automata, (), 109-120
[7] Doyen, L.; Henzinger, T.A.; Jobstmann, B.; Petrov, T., Interface theories with component reuse, (), 79-88
[8] Chakrabarti, A.; de Alfaro, L.; Henzinger, T.A.; Mang, F.Y.C., (), 414-427
[9] de Alfaro, L.; da Silva, L.D.; Faella, M.; Legay, A.; Roy, P.; Sorea, M., Sociable interfaces, (), 81-105 · Zbl 1171.68837
[10] Adler, B.T.; de Alfaro, L.; da Silva, L.D.; Faella, M.; Legay, A.; Raman, V.; Roy, P., Ticc: a tool for interface compatibility and composition, (), 59-62
[11] Jonsson, B.; Larsen, K.G., Specification and refinement of probabilistic processes, (), 266-277
[12] Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Form. asp. comput., 6, 5, 512-535, (1994) · Zbl 0820.68113
[13] Brázdil, T.; Forejt, V.; Kretínský, J.; Kucera, A., The satisfiability problem for probabilistic ctl, (), 391-402
[14] David, A.; Larsen, K.G.; Legay, A.; Nyman, U.; Wasowski, A., Methodologies for specification of real-time systems using timed i/o automata, (), 290-310 · Zbl 1312.68131
[15] de Alfaro, L.; Henzinger, T.A., Interface-based design, (), 83-104
[16] Fecher, H.; Leucker, M.; Wolf, V., Don’t know in probabilistic systems, (), 71-88 · Zbl 1178.68341
[17] Segala, R.; Lynch, N., Probabilistic simulations for probabilistic processes, (), 481-496
[18] H. Hansson, B. Jonsson, A calculus for communicating systems with time and probabitilies, in: IEEE Real-Time Systems Symposium, 1990, pp. 278-287.
[19] Jonsson, B.; Larsen, K.; Yi, W., Probabilistic extensions of process algebras, (), 681-710 · Zbl 1062.68081
[20] Hermanns, H., Interactive Markov chains: and the quest for quantified quality, (2002), Springer-Verlag Berlin, Heidelberg · Zbl 1012.68142
[21] Sen, K.; Viswanathan, M.; Agha, G., Model-checking Markov chains in the presence of uncertainties, (), 394-410 · Zbl 1180.68179
[22] Chatterjee, K.; Sen, K.; Henzinger, T.A., Model-checking omega-regular properties of interval Markov chains, (), 302-317 · Zbl 1138.68441
[23] Brown, C.W., Simple cad construction and its applications, J. symbolic comput., 31, 5, 521-547, (2001) · Zbl 0976.65023
[24] C.W. Brown, J.H. Davenport, The complexity of quantifier elimination and cylindrical algeraic decomposition, in: Symbolic and Algebraic Computation SSAC, Waterloo, ON, Canada, 2007, pp. 54-60. · Zbl 1190.68028
[25] Yanami, H.; Anai, H., Synrac: a Maple toolbox for solving real algebraic constraints, ACM commun. comput. algebra, 41, 3, 112-113, (2007)
[26] Basu, S., New results on quantifier elimination over real closed fields and applications to constraint databases, J. ACM, 46, 4, 537-555, (1999) · Zbl 1065.03507
[27] B. Caillaud, B. Delahaye, K.G. Larsen, A. Legay, M.L. Pedersen, A. Wąsowski, Decision problems for interval markov chains, Res. Rep. (2010). URL http://www.cs.aau.dk/ mikkelp/doc/IMCpaper.pdf.
[28] Beneš, N.; Křetínský, J.; Larsen, K.; Srba, J., On determinism in modal transition systems, Theoret. comput. sci., 410, 41, 4026-4043, (2009) · Zbl 1186.68314
[29] Katoen, J.; Klink, D.; Neuhäußer, M.R., Compositional abstraction for stochastic systems, (), 195-211 · Zbl 1262.68142
[30] Ciesinski, F.; Größer, M., On probabilistic computation tree logic, (), 147-188 · Zbl 1203.68096
[31] Haddad, S.; Pekergin, N., Using stochastic comparison for efficient model checking of uncertain Markov chains, (), 177-186
[32] Hermanns, H.; Herzog, U.; Katoen, J., Process algebra for performance evaluation, Theoret. comput. sci., 274, 1-2, 43-87, (2002) · Zbl 0992.68149
[33] Hillston, J., A compositional approach to performance modelling, (1996), Cambridge University Press
[34] Katoen, J.; Klink, D.; Leucker, M.; Wolf, V., Three-valued abstraction for continuous-time Markov chains, (), 311-324 · Zbl 1135.68476
[35] Andova, S., Process algebra with probabilistic choice, (), 111-129
[36] López, N.; Núñez, M., An overview of probabilistic process algebras and their equivalences, (), 89-123 · Zbl 1203.68115
[37] Hermanns, H.; Wachter, B.; Zhang, L., Probabilistic CEGAR, (), 162-175 · Zbl 1155.68438
[38] Hartfield, H.J., ()
[39] Abate, A.; D’Innocenzo, A.; Benedetto, M.D.D.; Sastry, S.S., Markov set-chains as abstractions of stochastic hybrid sytems, (), 1-15 · Zbl 1144.93367
[40] Altman, E., Constrained Markov decision processes, (1999), Chapman & Hall/CRC · Zbl 0963.90068
[41] Larsen, K.G.; Skou, A., Compositional verification of probabilistic processes, (), 456-471
[42] Raclet, J.-B.; Badouel, E.; Benveniste, A.; Caillaud, B.; Passerone, R., Why are modalities good for interface theories?, (), 119-127
[43] J.-B. Raclet, Quotient de spécifications pour la réutilisation de composants, Ph.D. Thesis, Université de Rennes I, december 2007 (in French).
[44] Raclet, J.-B., Residual for component specifications, (), 93-110
[45] Bhaduri, P., Synthesis of interface automata, (), 338-353 · Zbl 1141.68427
[46] David, A.; Larsen, K.G.; Legay, A.; Nyman, U.; Wąsowski, A., Timed i/o automata: a complete specification theory for real-time systems, (), 91-100 · Zbl 1361.68143
[47] Bertrand, N.; Pinchinat, S.; Raclet, J.-B., Refinement and consistency of timed modal specifications, (), 152-163 · Zbl 1234.68250
[48] Bertrand, N.; Legay, A.; Pinchinat, S.; Raclet, J.-B., A compositional approach on modal specifications for timed systems, (), 679-697
[49] Kwiatkowska, M.Z.; Norman, G.; Sproston, J.; Wang, F., Symbolic model checking for probabilistic timed automata, Inform. and comput., 205, 7, 1027-1077, (2007) · Zbl 1122.68075
[50] Delahaye, B.; Caillaud, B.; Legay, A., Probabilistic contracts: A compositional reasoning methodology for the design of stochastic systems, (), 223-232
[51] de Alfaro, L.; Henzinger, T.A.; Jhala, R., Compositional methods for probabilistic systems, (), 351-365 · Zbl 1006.68083
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.