{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,10]],"date-time":"2026-03-10T00:58:35Z","timestamp":1773104315798,"version":"3.50.1"},"publisher-location":"Cham","reference-count":78,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030451899","type":"print"},{"value":"9783030451905","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-45190-5_18","type":"book-chapter","created":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T09:03:02Z","timestamp":1587114182000},"page":"324-345","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":18,"title":["Farkas Certificates and Minimal Witnesses for Probabilistic Reachability Constraints"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7301-1550","authenticated-orcid":false,"given":"Florian","family":"Funke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1692-2408","authenticated-orcid":false,"given":"Simon","family":"Jantsch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5321-9343","authenticated-orcid":false,"given":"Christel","family":"Baier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,4,17]]},"reference":[{"key":"18_CR1","doi-asserted-by":"publisher","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J., Wimmer, R.: Counterexample generation for discrete-time Markov models: An introductory survey. In: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2014. pp. 65\u2013121 (2014), \nhttps:\/\/doi.org\/10.1007\/978-3-319-07317-0_3","DOI":"10.1007\/978-3-319-07317-0_3"},{"key":"18_CR2","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997)."},{"key":"18_CR3","unstructured":"de Alfaro, L.: Temporal logics for the specification of performance and reliability. In: STACS 97. pp. 165\u2013176. Springer, Berlin, Heidelberg (1997)."},{"key":"18_CR4","doi-asserted-by":"publisher","unstructured":"Aljazzar, H., Leitner-Fischer, F., Leue, S., Simeonov, D.: Dipro - A tool for probabilistic counterexample generation. In: Model Checking Software - 18th International SPIN Workshop 2011. pp. 183\u2013187 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-22306-8_13","DOI":"10.1007\/978-3-642-22306-8_13"},{"key":"18_CR5","doi-asserted-by":"publisher","unstructured":"Aljazzar, H., Leue, S.: Extended directed search for probabilistic timed reachability. In: Formal Modeling and Analysis of Timed Systems, 4th International Conference, FORMATS 2006. pp. 33\u201351 (2006), \nhttps:\/\/doi.org\/10.1007\/11867340_4","DOI":"10.1007\/11867340_4"},{"key":"18_CR6","doi-asserted-by":"publisher","unstructured":"Aljazzar, H., Leue, S.: Generation of counterexamples for model checking of Markov decision processes. In: Sixth International Conference on the Quantitative Evaluation of Systems, QEST 2009. pp. 197\u2013206 (2009), \nhttps:\/\/doi.org\/10.1109\/QEST.2009.10","DOI":"10.1109\/QEST.2009.10"},{"key":"18_CR7","doi-asserted-by":"publisher","unstructured":"Aljazzar, H., Leue, S.: Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Trans. Software Eng. 36(1), 37\u201360 (2010), \nhttps:\/\/doi.org\/10.1109\/TSE.2009.57","DOI":"10.1109\/TSE.2009.57"},{"key":"18_CR8","unstructured":"Amaldi, E., Kann, V.: On the approximability of minimizing nonzero variables or unsatisfied relations in linear systems. Theoretical Computer Science 209(1), 237\u2013260 (1998), \nhttp:\/\/www.sciencedirect.com\/science\/article\/pii\/S0304397597001151"},{"key":"18_CR9","doi-asserted-by":"publisher","unstructured":"Andr\u00e9s, M.E., D\u2019Argenio, P.R., van Rossum, P.: Significant diagnostic counterexamples in probabilistic model checking. In: Hardware and Software: Verification and Testing, 4th International Haifa Verification Conference, HVC 2008. pp. 129\u2013148 (2008), \nhttps:\/\/doi.org\/10.1007\/978-3-642-01702-5_15","DOI":"10.1007\/978-3-642-01702-5_15"},{"key":"18_CR10","doi-asserted-by":"publisher","unstructured":"Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of Algorithms 11(3), 441\u2013461 (1990), \nhttps:\/\/doi.org\/10.1016\/0196-6774(90)90021-6","DOI":"10.1016\/0196-6774(90)90021-6"},{"key":"18_CR11","doi-asserted-by":"publisher","unstructured":"Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration of arrangements and polyhedra. Discrete & Computational Geometry 8, 295\u2013313 (1992), \nhttps:\/\/doi.org\/10.1007\/BF02293050","DOI":"10.1007\/BF02293050"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Avis, D., Fukuda, K.: Reverse search for enumeration. Discrete Applied Mathematics 65, 21\u201346 (1993).","DOI":"10.1016\/0166-218X(95)00026-N"},{"key":"18_CR13","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge, MA (2008)."},{"key":"18_CR14","doi-asserted-by":"publisher","unstructured":"Balinski, M.L.: An algorithm for finding all vertices of convex polyhedral sets. Journal of the Society for Industrial and Applied Mathematics 9(1), 72\u201388 (1961), \nhttps:\/\/doi.org\/10.1137\/0109008","DOI":"10.1137\/0109008"},{"key":"18_CR15","doi-asserted-by":"publisher","unstructured":"Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L.D., Ghezzi, C.: From model checking to a temporal proof for partial models. In: Software Engineering and Formal Methods - 15th International Conference, SEFM 2017. pp. 54\u201369 (2017), \nhttps:\/\/doi.org\/10.1007\/978-3-319-66197-1_4","DOI":"10.1007\/978-3-319-66197-1_4"},{"key":"18_CR16","doi-asserted-by":"crossref","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Foundations of Software Technology and Theoretical Computer Science. pp. 499\u2013513. Springer, Berlin, Heidelberg (1995).","DOI":"10.21236\/ADA461346"},{"key":"18_CR17","doi-asserted-by":"publisher","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. Journal of the ACM 42(1), 269\u2013291 (1995), \nhttps:\/\/doi.org\/10.1145\/200836.200880","DOI":"10.1145\/200836.200880"},{"key":"18_CR18","doi-asserted-by":"publisher","unstructured":"Braitling, B., Wimmer, R., Becker, B., Jansen, N., \u00c1brah\u00e1m, E.: Counterexample generation for Markov chains using SMT-based bounded model checking. In: Formal Techniques for Distributed Systems - Joint 13th IFIP WG 6.1 International Conference, FMOODS 2011, and 31st IFIP WG 6.1 International Conference, FORTE 2011. pp. 75\u201389 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-21461-5_5","DOI":"10.1007\/978-3-642-21461-5_5"},{"key":"18_CR19","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmelik, M., Fellner, A., Kret\u00ednsk\u00fd, J.: Counterexample explanation by learning small strategies in Markov decision processes. In: Computer Aided Verification - 27th International Conference, CAV 2015. pp. 158\u2013177 (2015), \nhttps:\/\/doi.org\/10.1007\/978-3-319-21690-4_10","DOI":"10.1007\/978-3-319-21690-4_10"},{"key":"18_CR20","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov Decision Processes Using Learning Algorithms. In: Automated Technology for Verification and Analysis (ATVA 2014). pp. 98\u2013114 (2014), \nhttps:\/\/doi.org\/10.1007\/978-3-319-11936-6_8","DOI":"10.1007\/978-3-319-11936-6_8"},{"key":"18_CR21","doi-asserted-by":"publisher","unstructured":"Bremner, D., Fukuda, K., Marzetta, A.: Primal\u2013dual methods for vertex and facet enumeration. Discrete & Computational Geometry 20(3), 333\u2013357 (1998), \nhttps:\/\/doi.org\/10.1007\/PL00009389","DOI":"10.1007\/PL00009389"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Bussieck, M.R., L\u00fcbbecke, M.E.: The vertex set of a 0\/1 polytope is strongly $$\\cal{P}$$-enumerable. Computational Geometry Theory and Applications 11(2), 103\u2013109 (1998).","DOI":"10.1016\/S0925-7721(98)00021-2"},{"key":"18_CR23","doi-asserted-by":"publisher","unstructured":"Ceska, M., Hensel, C., Junges, S., Katoen, J.: Counterexample-driven synthesis for probabilistic program sketches. In: Formal Methods - The Next 30 Years - Third World Congress, FM 2019. pp. 101\u2013120 (2019), \nhttps:\/\/doi.org\/10.1007\/978-3-030-30942-8_8","DOI":"10.1007\/978-3-030-30942-8_8"},{"key":"18_CR24","doi-asserted-by":"publisher","unstructured":"Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic 12(1), 1:1\u20131:49 (2010), \nhttps:\/\/doi.org\/10.1145\/1838552.1838553","DOI":"10.1145\/1838552.1838553"},{"key":"18_CR25","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Chmelik, M., Daca, P.: CEGAR for qualitative analysis of probabilistic systems. In: Computer Aided Verification - 26th International Conference, CAV 2014. pp. 473\u2013490 (2014), \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_31","DOI":"10.1007\/978-3-319-08867-9_31"},{"key":"18_CR26","doi-asserted-by":"publisher","unstructured":"Ciesinski, F., Baier, C., Gr\u00f6\u00dfer, M., Klein, J.: Reduction techniques for model checking Markov decision processes. In: 2008 Fifth International Conference on Quantitative Evaluation of Systems. pp. 45\u201354 (2008). \nhttps:\/\/doi.org\/10.1109\/QEST.2008.45","DOI":"10.1109\/QEST.2008.45"},{"key":"18_CR27","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003), \nhttps:\/\/doi.org\/10.1145\/876638.876643","DOI":"10.1145\/876638.876643"},{"key":"18_CR28","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Jha, S., Lu, Y., Veith, H.: Tree-like counterexamples in model checking. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002). pp. 19\u201329 (2002), \nhttps:\/\/doi.org\/10.1109\/LICS.2002.1029814","DOI":"10.1109\/LICS.2002.1029814"},{"key":"18_CR29","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Veith, H.: Counterexamples revisited: Principles, algorithms, applications. In: Verification: Theory and Practice, Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday. pp. 208\u2013224 (2003), \nhttps:\/\/doi.org\/10.1007\/978-3-540-39910-0_9","DOI":"10.1007\/978-3-540-39910-0_9"},{"key":"18_CR30","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Computer Aided Verification, 15th International Conference, CAV 2003. pp. 420\u2013432 (2003)."},{"key":"18_CR31","doi-asserted-by":"publisher","unstructured":"Courcoubetis, C., Yannakakis, M.: Verifying temporal properties of finite-state probabilistic programs. In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science. pp. 338\u2013345. SFCS \u201988, IEEE Computer Society (1988), \nhttps:\/\/doi.org\/10.1109\/SFCS.1988.21950","DOI":"10.1109\/SFCS.1988.21950"},{"key":"18_CR32","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM 42(4), 857\u2013907 (1995), \nhttp:\/\/doi.acm.org\/10.1145\/210332.210339","DOI":"10.1145\/210332.210339"},{"key":"18_CR33","doi-asserted-by":"publisher","unstructured":"Damman, B., Han, T., Katoen, J.: Regular expressions for PCTL counterexamples. In: Fifth International Conference on the Quantitative Evaluaiton of Systems (QEST 2008). pp. 179\u2013188 (2008), \nhttps:\/\/doi.org\/10.1109\/QEST.2008.11","DOI":"10.1109\/QEST.2008.11"},{"key":"18_CR34","doi-asserted-by":"publisher","unstructured":"D\u2019Argenio, P.R., Jeannet, B., Jensen, H.E., Larsen, K.G.: Reachability analysis of probabilistic systems by successive refinements. In: Process Algebra and Probabilistic Methods, Performance Modeling and Verification: Joint International Workshop, PAPM-PROBMIV 2001. pp. 39\u201356 (2001), \nhttps:\/\/doi.org\/10.1007\/3-540-44804-7_3","DOI":"10.1007\/3-540-44804-7_3"},{"key":"18_CR35","doi-asserted-by":"publisher","unstructured":"Dyer, M.E.: The complexity of vertex enumeration methods. Mathematics of Operations Research 8(3), 381\u2013402 (1983), \nhttps:\/\/doi.org\/10.1287\/moor.8.3.381","DOI":"10.1287\/moor.8.3.381"},{"key":"18_CR36","doi-asserted-by":"publisher","unstructured":"Dyer, M.E., Proll, L.G.: An algorithm for determining all extreme points of a convex polytope. Mathematical Programming 12(1), 81\u201396 (1977), \nhttps:\/\/doi.org\/10.1007\/BF01593771","DOI":"10.1007\/BF01593771"},{"key":"18_CR37","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M.Y., Yannakakis, M.: Multi-Objective Model Checking of Markov Decision Processes. Logical Methods in Computer Science 4(4) (2008), \nhttps:\/\/lmcs.episciences.org\/990"},{"key":"18_CR38","unstructured":"Farkas, J.: Theorie der einfachen ungleichungen. Journal f\u00fcr die reine und angewandte Mathematik 124, 1\u201327 (1902), \nhttp:\/\/eudml.org\/doc\/149129"},{"key":"18_CR39","doi-asserted-by":"publisher","unstructured":"Forejt, V., Kwiatkowska, M.Z., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Tools and Algorithms for the Construction and Analysis of Systems - 17th International Conference, TACAS 2011. pp. 112\u2013127 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-19835-9_11","DOI":"10.1007\/978-3-642-19835-9_11"},{"key":"18_CR40","unstructured":"Fukuda, K., Liebling, T.M., Margot, F.: Analysis of backtrack algorithms for listing all vertices and all faces of a convex polyhedron. Computational Geometry 8(1), 1\u201312 (1997), \nhttp:\/\/www.sciencedirect.com\/science\/article\/pii\/0925772195000496"},{"key":"18_CR41","doi-asserted-by":"publisher","unstructured":"Fukuda, K., Prodon, A.: Double description method revisited. In: Combinatorics and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference 1995. pp. 91\u2013111 (1995), \nhttps:\/\/doi.org\/10.1007\/3-540-61576-8_77","DOI":"10.1007\/3-540-61576-8_77"},{"key":"18_CR42","unstructured":"Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for probabilistic reachability constraints (2019), \nhttps:\/\/arxiv.org\/abs\/1910.10636\n\n."},{"key":"18_CR43","unstructured":"Gurobi Optimization LLC, L.: Gurobi optimizer reference manual (2019), \nhttp:\/\/www.gurobi.com\n\n."},{"key":"18_CR44","doi-asserted-by":"publisher","unstructured":"Han, T., Katoen, J.: Counterexamples in probabilistic model checking. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007). pp. 72\u201386 (2007), \nhttps:\/\/doi.org\/10.1007\/978-3-540-71209-1_8","DOI":"10.1007\/978-3-540-71209-1_8"},{"key":"18_CR45","doi-asserted-by":"publisher","unstructured":"Han, T., Katoen, J., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering 35(2), 241\u2013257 (2009), \nhttps:\/\/doi.org\/10.1109\/TSE.2009.5","DOI":"10.1109\/TSE.2009.5"},{"key":"18_CR46","doi-asserted-by":"crossref","unstructured":"Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program. ACM Transactions on Programming Languages and Systems 5(3), 356\u2013380 (1983), \nhttp:\/\/doi.acm.org\/10.1145\/2166.357214","DOI":"10.1145\/2166.357214"},{"key":"18_CR47","doi-asserted-by":"publisher","unstructured":"Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Types for Proofs and Programs, International Workshop TYPES\u201993. pp. 127\u2013165 (1993), \nhttps:\/\/doi.org\/10.1007\/3-540-58085-9_75","DOI":"10.1007\/3-540-58085-9_75"},{"key":"18_CR48","doi-asserted-by":"publisher","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Computer Aided Verification, 20th International Conference, CAV 2008. pp. 162\u2013175 (2008), \nhttps:\/\/doi.org\/10.1007\/978-3-540-70545-1_16","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"18_CR49","doi-asserted-by":"publisher","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Katelaan, J., Wimmer, R., Katoen, J., Becker, B.: Hierarchical counterexamples for discrete-time Markov chains. In: Automated Technology for Verification and Analysis, 9th International Symposium, ATVA 2011. pp. 443\u2013452 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-24372-1_33","DOI":"10.1007\/978-3-642-24372-1_33"},{"key":"18_CR50","doi-asserted-by":"publisher","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Volk, M., Wimmer, R., Katoen, J., Becker, B.: The COMICS tool - computing minimal counterexamples for dtmcs. In: Automated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012. pp. 349\u2013353 (2012), \nhttps:\/\/doi.org\/10.1007\/978-3-642-33386-6_27","DOI":"10.1007\/978-3-642-33386-6_27"},{"key":"18_CR51","doi-asserted-by":"publisher","unstructured":"Jansen, N., \u00c1brah\u00e1m, E., Zajzon, B., Wimmer, R., Schuster, J., Katoen, J., Becker, B.: Symbolic counterexample generation for discrete-time Markov chains. In: Formal Aspects of Component Software, 9th International Symposium, FACS 2012. pp. 134\u2013151 (2012), \nhttps:\/\/doi.org\/10.1007\/978-3-642-35861-6_9","DOI":"10.1007\/978-3-642-35861-6_9"},{"key":"18_CR52","doi-asserted-by":"publisher","unstructured":"Jansen, N., Wimmer, R., \u00c1brah\u00e1m, E., Zajzon, B., Katoen, J., Becker, B., Schuster, J.: Symbolic counterexample generation for large discrete-time Markov chains. Science of Computer Programming 91, 90\u2013114 (2014), \nhttps:\/\/doi.org\/10.1016\/j.scico.2014.02.001","DOI":"10.1016\/j.scico.2014.02.001"},{"key":"18_CR53","doi-asserted-by":"publisher","unstructured":"Jr., M.C., Jansen, N., Junges, S., Katoen, J.: Shepherding hordes of Markov chains. In: Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019. pp. 172\u2013190 (2019), \nhttps:\/\/doi.org\/10.1007\/978-3-030-17465-1_10","DOI":"10.1007\/978-3-030-17465-1_10"},{"key":"18_CR54","unstructured":"Karp, R.M.: Reducibility among combinatorial problems. In: Complexity of Computer Computations: Proceedings of a symposium on the Complexity of Computer Computations, 1972. pp. 85\u2013103. Springer, US, Boston, MA (1972)."},{"key":"18_CR55","doi-asserted-by":"publisher","unstructured":"Khachiyan, L., Boros, E., Borys, K., Elbassioni, K., Gurvich, V.: Generating all vertices of a polyhedron is hard. Discrete & Computational Geometry 39(1), 174\u2013190 (2008), \nhttps:\/\/doi.org\/10.1007\/s00454-008-9050-5","DOI":"10.1007\/s00454-008-9050-5"},{"key":"18_CR56","doi-asserted-by":"publisher","unstructured":"Kuntz, M., Leitner-Fischer, F., Leue, S.: From probabilistic counterexamples via causality to fault trees. In: Proceedings of the 30th International Conference on Computer Safety, Reliability, and Security (SAFECOMP). pp. 71\u201384 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-24270-0_6","DOI":"10.1007\/978-3-642-24270-0_6"},{"key":"18_CR57","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: From complementation to certification. In: Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004. pp. 591\u2013606 (2004), \nhttps:\/\/doi.org\/10.1007\/978-3-540-24730-2_43","DOI":"10.1007\/978-3-540-24730-2_43"},{"key":"18_CR58","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Computer Aided Verification - 23rd International Conference, CAV 2011. pp. 585\u2013591 (2011), \nhttps:\/\/doi.org\/10.1007\/978-3-642-22110-1_47","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"18_CR59","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In: Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012. pp. 203\u2013204 (2012), \nhttps:\/\/doi.org\/10.1109\/QEST.2012.14","DOI":"10.1109\/QEST.2012.14"},{"key":"18_CR60","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Segala, R.: Automated verification of a randomized distributed consensus protocol using cadence SMV and PRISM. In: Computer Aided Verification, 13th International Conference, CAV 2001. pp. 194\u2013206 (2001), \nhttps:\/\/doi.org\/10.1007\/3-540-44585-4_17","DOI":"10.1007\/3-540-44585-4_17"},{"key":"18_CR61","doi-asserted-by":"publisher","unstructured":"Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation 205(7), 1027\u20131077 (2007), \nhttps:\/\/doi.org\/10.1016\/j.ic.2007.01.004","DOI":"10.1016\/j.ic.2007.01.004"},{"key":"18_CR62","unstructured":"Mangasarian, O.: Nonlinear Programming. Classics in Applied Mathematics, Society for Industrial and Applied Mathematics (1994)."},{"key":"18_CR63","doi-asserted-by":"crossref","unstructured":"Mattheiss, T.H.: An algorithm for determining irrelevant constraints and all vertices in systems of linear inequalities. Operations Research 21(1), 247\u2013260 (1973), \nhttp:\/\/www.jstor.org\/stable\/169104","DOI":"10.1287\/opre.21.1.247"},{"key":"18_CR64","doi-asserted-by":"publisher","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review 5(2), 119\u2013161 (2011), \nhttps:\/\/doi.org\/10.1016\/j.cosrev.2010.09.009","DOI":"10.1016\/j.cosrev.2010.09.009"},{"key":"18_CR65","unstructured":"Naiman, D.Q., Scheinerman, E.R.: Arbitrage and geometry. Preprint (2017), \nhttps:\/\/arxiv.org\/abs\/1709.07446\n\n."},{"key":"18_CR66","doi-asserted-by":"publisher","unstructured":"Namjoshi, K.S.: Certifying model checkers. In: Computer Aided Verification, 13th International Conference, CAV 2001. pp. 2\u201313 (2001), \nhttps:\/\/doi.org\/10.1007\/3-540-44585-4_2","DOI":"10.1007\/3-540-44585-4_2"},{"key":"18_CR67","doi-asserted-by":"publisher","unstructured":"Peled, D.A., Pnueli, A., Zuck, L.D.: From falsification to verification. In: FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science. pp. 292\u2013304 (2001), \nhttps:\/\/doi.org\/10.1007\/3-540-45294-X_25","DOI":"10.1007\/3-540-45294-X_25"},{"key":"18_CR68","doi-asserted-by":"publisher","unstructured":"Provan, J.S.: Efficient enumeration of the vertices of polyhedra associated with network LP\u2019s. Mathematical Programming 63(1), 47\u201364 (1994), \nhttps:\/\/doi.org\/10.1007\/BF01582058","DOI":"10.1007\/BF01582058"},{"key":"18_CR69","doi-asserted-by":"publisher","unstructured":"Reiter, M.K., Rubin, A.D.: Crowds: Anonymity for web transactions. ACM Transactions on Information and System Security 1(1), 66\u201392 (1998), \nhttps:\/\/doi.org\/10.1145\/290163.290168","DOI":"10.1145\/290163.290168"},{"key":"18_CR70","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons Inc., New York, NY, USA (1986)."},{"key":"18_CR71","unstructured":"Schrijver, A.: A course in combinatorial optimization. Lecture notes (2017), \nhttps:\/\/homepages.cwi.nl\/~lex\/files\/dict.pdf\n\n."},{"key":"18_CR72","doi-asserted-by":"crossref","unstructured":"Shmatikov, V.: Probabilistic analysis of an anonymity system. Journal of Computer Security 12(3-4), 355\u2013377 (2004).","DOI":"10.3233\/JCS-2004-123-403"},{"key":"18_CR73","doi-asserted-by":"publisher","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite state programs. In: Proceedings of the 26th Annual Symposium on Foundations of Computer Science. pp. 327\u2013338. SFCS \u201985, IEEE Computer Society (1985), \nhttps:\/\/doi.org\/10.1109\/SFCS.1985.12","DOI":"10.1109\/SFCS.1985.12"},{"key":"18_CR74","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings of the Symposium on Logic in Computer Science (LICS 86). pp. 332\u2013344 (1986)."},{"key":"18_CR75","doi-asserted-by":"publisher","unstructured":"Vohra, R.V.: The ubiquitous farkas lemma. In: Perspectives in Operations Research: Papers in Honor of Saul Gass\u2019 80th Birthday. pp. 199\u2013210. Springer US, Boston, MA (2006), \nhttps:\/\/doi.org\/10.1007\/978-0-387-39934-8_11","DOI":"10.1007\/978-0-387-39934-8_11"},{"key":"18_CR76","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Braitling, B., Becker, B.: Counterexample generation for discrete-time Markov chains using bounded model checking. In: Verification, Model Checking, and Abstract Interpretation, 10th International Conference, VMCAI 2009. pp. 366\u2013380 (2009), \nhttps:\/\/doi.org\/10.1007\/978-3-540-93900-9_29","DOI":"10.1007\/978-3-540-93900-9_29"},{"key":"18_CR77","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Becker, B., Katoen, J.: Minimal critical subsystems for discrete-time markov models. In: Tools and Algorithms for the Construction and Analysis of Systems - 18th International Conference, TACAS 2012. pp. 299\u2013314 (2012), \nhttps:\/\/doi.org\/10.1007\/978-3-642-28756-5_21","DOI":"10.1007\/978-3-642-28756-5_21"},{"key":"18_CR78","doi-asserted-by":"publisher","unstructured":"Wimmer, R., Jansen, N., \u00c1brah\u00e1m, E., Katoen, J., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theoretical Computer Science 549, 61\u2013100 (2014), \nhttps:\/\/doi.org\/10.1016\/j.tcs.2014.06.020","DOI":"10.1016\/j.tcs.2014.06.020"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-45190-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,20]],"date-time":"2020-08-20T13:12:10Z","timestamp":1597929130000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-45190-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030451899","9783030451905"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-45190-5_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 April 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Dublin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 April 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 April 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2020\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Easychair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"155","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"26% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"14","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference could not take place due to the COVID-19 pandemic. There was an online event on July 2, 2020.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}