×

zbMATH — the first resource for mathematics

Measuring and synthesizing systems in probabilistic environments. (English) Zbl 1321.68344

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68Q87 Probability in computer science (algorithm analysis, random structures, phase transitions, etc.)
Software:
CESAR; GLPK; MCGP; QUASY
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] R. Alur, A. Degorre, O. Maler, and G. Weiss. 2009. On omega-languages defined by mean-payoff conditions. In Proceedings of FOSSACS. Lecture Notes in Computer Science, vol. 5504, Springer, 333–347. · Zbl 1234.68248
[2] C. Baier, M. Grösser, M. Leucker, B. Bollig, and F. Ciesinski. 2004. Controller synthesis for probabilistic systems. In Proceedings of IFIP TCS. Kluwer, 493–506. · Zbl 1073.93037
[3] C. Baier and J.-P. Katoen. 2008. Principles of Model Checking (Representation and Mind Series). MIT Press.
[4] A. Bianco and L. de Alfaro. 1995. Model checking of probabilistic and nondeterministic systems. In Proceedings of FSTTCS 95. Lecture Notes in Computer Science, vol. 1026, Springer, 499–513. · Zbl 1354.68167
[5] P. Billingsley, Ed. 1995. Probability and Measure. Wiley-Interscience. · Zbl 0822.60002
[6] R. Bloem, K. Chatterjee, T. Henzinger, and B. Jobstmann. 2009a. Better quality in synthesis through quantitative objectives. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 5643, Springer, 140–156. · Zbl 1242.68151
[7] R. Bloem, K. Greimel, T. Henzinger, and B. Jobstmann. 2009b. Synthesizing robust systems. In Proceedings of FMCAD. IEEE, 85–92. · Zbl 1302.93079
[8] A. Chakrabarti, K. Chatterjee, T. Henzinger, O. Kupferman, and R. Majumdar. 2005. Verifying quantitative properties using bound functions. In Proceedings of CHARME. Lecture Notes in Computer Science, vol. 3725, Springer, 50–64. · Zbl 1159.68313
[9] A. Chakrabarti, L. de Alfaro, T. Henzinger, and M. Stoelinga. 2003. Resource interfaces. In Proceedings of EMSOFT. Lecture Notes in Computer Science, vol. 2855. Springer, 117–133.
[10] K. Chatterjee, L. de Alfaro, M. Faella, T. Henzinger, R. Majumdar, and M. Stoelinga. 2006. Compositional quantitative reasoning. In Proceedings of QEST. IEEE, 179–188.
[11] K. Chatterjee and L. Doyen. 2011a. Energy and mean-payoff parity Markov decision processes. In Proceedings of MFCS. 206–218. · Zbl 1343.90107
[12] K. Chatterjee and L. Doyen. 2011b. Games and Markov decision processes with mean-payoff parity and energy parity objectives. In Proceedings of MEMICS. 37–46. · Zbl 1343.90107
[13] K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj. 2014. Perfect-information stochastic mean-payoff parity games. In Proceedings of FoSSaCS. 210–225. · Zbl 1405.68225
[14] K. Chatterjee, L. Doyen, and T. A. Henzinger. 2010a. Expressiveness and closure properties for quantitative languages. Log. Meth. Comput. Sci. 6, 3. · Zbl 1200.68135 · doi:10.2168/LMCS-6(3:10)2010
[15] K. Chatterjee, L. Doyen, and T. A. Henzinger. 2010b. Quantitative languages. ACM Trans. Comput. Log. 11, 4. · Zbl 1351.68155 · doi:10.1145/1805950.1805953
[16] K. Chatterjee and M. Henzinger. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In Proceedings of SODA. ACM-SIAM, 1318–1336. · Zbl 1374.68272
[17] K. Chatterjee and M. Henzinger. 2012. An O(n2) algorithm for alternating Büchi games. In Proceedings of SODA. ACM-SIAM, 1386–1399.
[18] K. Chatterjee and M. Henzinger. 2014. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. JACM, 61, 3, Article 15. DOI 10.1145/2597631 · Zbl 1295.91019 · doi:10.1145/2597631
[19] K. Chatterjee, M. Henzinger, M. Joglekar, and N. Shah. 2013. Symbolic algorithms for qualitative analysis of Markov decision processes with Büchi objectives. Form. Meth. Syst. Design 42, 3, 301–327. · Zbl 1291.68251 · doi:10.1007/s10703-012-0180-2
[20] K. Chatterjee, T. Henzinger, and M. Jurdzinski. 2005. Mean-payoff parity games. In Proceedings of LICS. IEEE, 178–187.
[21] K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. 2010c. Measuring and synthesizing systems in probabilistic environments. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 6174, Springer, 380–395. · Zbl 1321.68344
[22] K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. 2011. Quasy: Quantitative synthesis tool. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 6605, Springer, 267–271. · Zbl 1316.68071
[23] K. Chatterjee, M. Jurdziński, and T. Henzinger. 2003. Simple stochastic parity games. In Proceedings of CSL’03. Lecture Notes in Computer Science, vol. 2803, Springer, 100–113. · Zbl 1116.68493
[24] K. Chatterjee, M. Jurdziński, and T. Henzinger. 2004. Quantitative stochastic parity games. In Proceedings of SODA. ACM-SIAM, 121–130. · Zbl 1318.91027
[25] K. Chatterjee and J. Lacki. 2013. Faster algorithms for Markov decision processes with low treewidth. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 8044, Springer, 543–558.
[26] C.-H. Cheng, M. Geisinger, H. Ruess, C. Buckl, and A. Knoll. 2012. MGSyn: Automatic synthesis for industrial automation. In Proceedings of CAV. 658–664.
[27] A. Church. 1962. Logic, arithmetic and automata. In Proceedings of the International Mathematical Congress. · Zbl 0116.33604
[28] E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Workshop on Logic of Programs. 52–71.
[29] C. Courcoubetis and M. Yannakakis. 1995. The complexity of probabilistic verification. J. ACM 42, 4, 857–907. · Zbl 0885.68109 · doi:10.1145/210332.210339
[30] P. Cousot and R. Cousot. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of POPL. ACM, 238–252.
[31] R. Cuninghame-Green. 1979. Minimax Algebra. In Lecture Notes in Economics and Mathematical Systems, vol. 166. Springer-Verlag. · Zbl 0399.90052
[32] L. de Alfaro. 1997a. Formal verification of probabilistic systems. Ph.D. thesis, Stanford University.
[33] L. de Alfaro. 1997b. Temporal logics for the specification of performance and reliability. In Proceedings of STACS’97. Lecture Notes in Computer Science, vol. 1200, Springer, 165–176.
[34] L. de Alfaro. 1998. Stochastic transition systems. In Proceedings of CONCUR. Lecture Notes in Computer Science, vol. 1466, Springer, 423–438.
[35] L. de Alfaro., T. Henzinger, and R. Majumdar. 2003. Discounting the future in systems theory. In Proceedings of ICALP. Lecture Notes in Computer Science, vol. 2719, Springer, 1022–1037. · Zbl 1039.68087
[36] L. de Alfaro, R. Majumdar, V. Raman, and M. Stoelinga. 2007. Game relations and metrics. In Proceedings of LICS. IEEE, 99–108. · Zbl 1147.68056
[37] J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. 1999. Metrics for labelled markov systems. In Proceedings of CONCUR. Lecture Notes in Computer Science, vol. 1664, Springer, 258–273. · Zbl 0939.68081
[38] M. Droste and P. Gastin. 2007. Weighted automata and weighted logics. Theoret. Comput. Sci. 380, 69–86. · Zbl 1118.68076 · doi:10.1016/j.tcs.2007.02.055
[39] M. Droste, W. Kuich, and G. Rahonis. 2008. Multi-valued MSO logics over words and trees. Fund. Inf. 84, 305–327. · Zbl 1157.03016
[40] M. Droste, W. Kuich, and H. Vogler. 2009. Handbook of Weighted Automata. Springer. · Zbl 1200.68001 · doi:10.1007/978-3-642-01492-5
[41] J. Filar and K. Vrieze. 1996. Competitive Markov Decision Processes. Springer. · Zbl 0934.91002 · doi:10.1007/978-1-4612-4054-9
[42] S. Fortune, J. Hopcroft, and J. Wyllie. 1980. The directed subgraph homeomorphism problem. Theoret. Comput. Sci. 10, 2, 111–121. · Zbl 0419.05028 · doi:10.1016/0304-3975(80)90009-2
[43] S. Gaubert. 1997. Methods and applications of (max, +) linear algebra. In Proceedings of STACS. Lecture Notes in Computer Science, vol. 1200, Springer, 261–282.
[44] GLPK. GLPK (gnu linear programming kit). http://www.gnu.org/software/glpk/.
[45] B. R. Haverkort. 1998. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley & Sons, Inc., New York, NY, USA. · doi:10.1002/0470841923
[46] G. Katz and D. Peled. 2010. Code mutation in verification and automatic code correction. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 6015, Springer, 435–450.
[47] V. King, O. Kupferman, and M. Y. Vardi. 2001. On the complexity of parity word automata. In Proceedings of FOSSACS. Lecture Notes in Computer Science, vol. 2030, Springer, 276–286. · Zbl 0978.68077
[48] O. Kupferman and Y. Lustig. 2007. Lattice automata. In Proceedings of VMCAI. Lecture Notes in Computer Science, vol. 4349. Springer, 199–213. · Zbl 1132.68455
[49] M. Kwiatkowska, G. Norman, and D. Parker. 2009. PRISM: Probabilistic model checking for performance and reliability analysis. ACM SIGMETRICS Perform. Eval. Rev.
[50] P. Niebert, D. Peled, and A. Pnueli. 2008. Discriminative model checking. In Proceedings of CAV. Lecture Notes in Computer Science, vol. 5123, Springer, 504–516. · Zbl 1155.68444
[51] R. Parr and S. Russell. 1997. Reinforcement learning with hierarchies of machines. In Proceedings of NIPS. MIT Press, 1043–1049.
[52] A. Pnueli. 1977. The temporal logic of programs. In Proceedings of FOCS. IEEE, 46–57.
[53] A. Pnueli and R. Rosner. 1989. On the synthesis of a reactive module. In Proceedings of POPL. ACM, 179–190. · Zbl 0686.68015
[54] M. Puterman. 1994. Markov Decision Processes. John Wiley & Sons, Inc. New York, NY. · Zbl 0829.90134 · doi:10.1002/9780470316887
[55] J.-P. Queille and J. Sifakis. 1982. Specification and verification of concurrent systems in CESAR. In Proceedings of Symposium on Programming. Lecture Notes in Computer Science, vol. 137, Springer, 337–351. · Zbl 0482.68028
[56] P. J. G. Ramadge and W. M. Wonham. 1989. The control of discrete event systems. IEEE Trans. Cont. Theory 77, 81–98.
[57] S. Safra. 1988. On the complexity of ω-automata. In Proceedings of FOCS. IEEE, 319–327.
[58] M. Vardi and P. Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of LICS. IEEE, 322–331.
[59] R. Wimmer, B. Braitling, B. Becker, E. M. Hahn, P. Crouzen, H. Hermanns, A. Dhama, and O. Theel. 2010. Symblicit calculation of long-run averages for concurrent probabilistic systems. In Proceedings of QEST. IEEE, 27–36.
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.