×

zbMATH — the first resource for mathematics

Abstract probabilistic automata. (English) Zbl 1317.68095
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 324-339 (2011).
Summary: Probabilistic Automata (PAs) are a widely-recognized mathematical framework for the specification and analysis of systems with non-deterministic and stochastic behaviors. This paper proposes Abstract Probabilistic Automata (APAs), that is a novel abstraction model for PAs. In APAs uncertainty of the non-deterministic choices is modeled by may/must modalities on transitions while uncertainty of the stochastic behaviour is expressed by (underspecified) stochastic constraints. We have developed a complete abstraction theory for PAs, and also propose the first specification theory for them. Our theory supports both satisfaction and refinement operators, together with classical stepwise design operators. In addition, we study the link between specification theories and abstraction in avoiding the state-space explosion problem.
For the entire collection see [Zbl 1206.68013].

MSC:
68Q45 Formal languages and automata
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 112–126. Springer, Heidelberg (2009) · Zbl 1250.68117 · doi:10.1007/978-3-642-03466-4_7
[2] Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Decision Problems for Interval Markov Chains (2010), http://www.cs.aau.dk/ mikkelp/doc/IMCpaper.pdf (Research report)
[3] Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Compositional design methodology with constraint Markov chains. In: QEST. IEEE, Los Alamitos (2010)
[4] Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wąsowski, A.: Compositional design methodology with constraint Markov chains. Submitted to TCS. Elsevier, Amsterdam (2010) · doi:10.1109/QEST.2010.23
[5] Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Analyzing security protocols using time-bounded task-pioas. Discrete Event Dynamic Systems 18(1), 111–159 (2008) · Zbl 1161.93320 · doi:10.1007/s10626-007-0032-1
[6] Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 371–385. Springer, Heidelberg (2002) · Zbl 1012.68127 · doi:10.1007/3-540-45694-5_25
[7] Cheung, L., Lynch, N.A., Segala, R., Vaandrager, F.W.: Switched pioa: Parallel composition via distributed scheduling. TCS 365(1-2), 83–108 (2006) · Zbl 1118.68038 · doi:10.1016/j.tcs.2006.07.033
[8] Cheung, L., Stoelinga, M., Vaandrager, F.W.: A testing scenario for probabilistic processes. J. ACM 54(6) (2007) · Zbl 1326.68138 · doi:10.1145/1314690.1314693
[9] de Alfaro, L., Henzinger, T.A.: Interface-based design. In: Engineering Theories of Software-intensive Systems. NATO Science Series: Mathematics, Physics, and Chemistry, vol. 195, pp. 83–104. Springer, Heidelberg (2005) · doi:10.1007/1-4020-3532-2_3
[10] Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata (2010), http://perso.bretagne.ens-cachan.fr/ delahaye/VMCAI11-long.pdf
[11] Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006) · Zbl 1178.68341 · doi:10.1007/11691617_5
[12] Jansen, D.N., Hermanns, H., Katoen, J.-P.: A probabilistic extension of uml statecharts. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 355–374. Springer, Heidelberg (2002) · Zbl 1278.68226 · doi:10.1007/3-540-45739-9_21
[13] Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE, Los Alamitos (1991)
[14] Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE, Los Alamitos (1991)
[15] Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 316–329. Springer, Heidelberg (2007) · Zbl 1135.68476 · doi:10.1007/978-3-540-73368-3_37
[16] Katoen, J.-P., Klink, D., Neuhäußer, M.R.: Compositional abstraction for stochastic systems. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 195–211. Springer, Heidelberg (2009) · Zbl 1262.68142 · doi:10.1007/978-3-642-04368-0_16
[17] Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007) · Zbl 1187.68296 · doi:10.1007/978-3-540-71316-6_6
[18] Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE, Los Alamitos (1988)
[19] Larsen, K.G.: Modal specifications. In: AVMFSS, pp. 232–246. Springer, Heidelberg (1989)
[20] Parma, A., Segala, R.: Axiomatization of trace semantics for stochastic nondeterministic processes. In: QEST, pp. 294–303. IEEE, Los Alamitos (2004)
[21] Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal interfaces: unifying interface automata and modal specifications. In: EMSOFT, pp. 87–96. ACM, New York (2009) · doi:10.1145/1629335.1629348
[22] Segala, R.: Probability and nondeterminism in operational models of concurrency. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 64–78. Springer, Heidelberg (2006) · Zbl 1151.68553 · doi:10.1007/11817949_5
[23] Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. NJC 2, 250–273 (1995) · Zbl 0839.68067
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.