342
F. Funke et al.
tions of Computer Science. pp. 338–345. SFCS ’88, IEEE Computer Society (1988),
https://doi.org/10.1109/SFCS.1988.21950
32. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification.
Journal of the ACM 42(4), 857–907 (1995), http://doi.acm.org/10.1145/210332.
210339
33. 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–188 (2008), https://doi.org/10.1109/QEST.2008.11
34. D’Argenio, 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–56 (2001), https://doi.org/10.1007/3-540-44804-7 3
35. Dyer, M.E.: The complexity of vertex enumeration methods. Mathematics of
Operations Research 8(3), 381–402 (1983), https://doi.org/10.1287/moor.8.3.381
36. Dyer, M.E., Proll, L.G.: An algorithm for determining all extreme points of a
convex polytope. Mathematical Programming 12(1), 81–96 (1977), https://doi.org/
10.1007/BF01593771
37. 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), https://lmcs.episciences.org/990
38. Farkas, J.: Theorie der einfachen ungleichungen. Journal f¨ ur die reine und angewandte Mathematik 124, 1–27 (1902), http://eudml.org/doc/149129
39. 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–127 (2011), https://doi.org/10.1007/978-3-642-19835-9 11
40. 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–12 (1997), http://www.sciencedirect.com/science/article/pii/0925772195000496
41. Fukuda, K., Prodon, A.: Double description method revisited. In: Combinatorics
and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference
1995. pp. 91–111 (1995), https://doi.org/10.1007/3-540-61576-8 77
42. Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for
probabilistic reachability constraints (2019), https://arxiv.org/abs/1910.10636
43. Gurobi Optimization LLC, L.: Gurobi optimizer reference manual (2019), http:
//www.gurobi.com
44. Han, T., Katoen, J.: Counterexamples in probabilistic model checking. In: Tools
and Algorithms for the Construction and Analysis of Systems (TACAS 2007). pp.
72–86 (2007), https://doi.org/10.1007/978-3-540-71209-1 8
45. Han, T., Katoen, J., Damman, B.: Counterexample generation in probabilistic
model checking. IEEE Transactions on Software Engineering 35(2), 241–257 (2009),
https://doi.org/10.1109/TSE.2009.5
46. Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program.
ACM Transactions on Programming Languages and Systems 5(3), 356–380 (1983),
http://doi.acm.org/10.1145/2166.357214
47. Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol.
In: Types for Proofs and Programs, International Workshop TYPES’93. pp. 127–165
(1993), https://doi.org/10.1007/3-540-58085-9 75
48. Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Computer Aided
Verification, 20th International Conference, CAV 2008. pp. 162–175 (2008), https:
//doi.org/10.1007/978-3-540-70545-1 16
F. Funke et al.
tions of Computer Science. pp. 338–345. SFCS ’88, IEEE Computer Society (1988),
https://doi.org/10.1109/SFCS.1988.21950
32. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification.
Journal of the ACM 42(4), 857–907 (1995), http://doi.acm.org/10.1145/210332.
210339
33. 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–188 (2008), https://doi.org/10.1109/QEST.2008.11
34. D’Argenio, 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–56 (2001), https://doi.org/10.1007/3-540-44804-7 3
35. Dyer, M.E.: The complexity of vertex enumeration methods. Mathematics of
Operations Research 8(3), 381–402 (1983), https://doi.org/10.1287/moor.8.3.381
36. Dyer, M.E., Proll, L.G.: An algorithm for determining all extreme points of a
convex polytope. Mathematical Programming 12(1), 81–96 (1977), https://doi.org/
10.1007/BF01593771
37. 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), https://lmcs.episciences.org/990
38. Farkas, J.: Theorie der einfachen ungleichungen. Journal f¨ ur die reine und angewandte Mathematik 124, 1–27 (1902), http://eudml.org/doc/149129
39. 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–127 (2011), https://doi.org/10.1007/978-3-642-19835-9 11
40. 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–12 (1997), http://www.sciencedirect.com/science/article/pii/0925772195000496
41. Fukuda, K., Prodon, A.: Double description method revisited. In: Combinatorics
and Computer Science, 8th Franco-Japanese and 4th Franco-Chinese Conference
1995. pp. 91–111 (1995), https://doi.org/10.1007/3-540-61576-8 77
42. Funke, F., Jantsch, S., Baier, C.: Farkas certificates and minimal witnesses for
probabilistic reachability constraints (2019), https://arxiv.org/abs/1910.10636
43. Gurobi Optimization LLC, L.: Gurobi optimizer reference manual (2019), http:
//www.gurobi.com
44. Han, T., Katoen, J.: Counterexamples in probabilistic model checking. In: Tools
and Algorithms for the Construction and Analysis of Systems (TACAS 2007). pp.
72–86 (2007), https://doi.org/10.1007/978-3-540-71209-1 8
45. Han, T., Katoen, J., Damman, B.: Counterexample generation in probabilistic
model checking. IEEE Transactions on Software Engineering 35(2), 241–257 (2009),
https://doi.org/10.1109/TSE.2009.5
46. Hart, S., Sharir, M., Pnueli, A.: Termination of probabilistic concurrent program.
ACM Transactions on Programming Languages and Systems 5(3), 356–380 (1983),
http://doi.acm.org/10.1145/2166.357214
47. Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol.
In: Types for Proofs and Programs, International Workshop TYPES’93. pp. 127–165
(1993), https://doi.org/10.1007/3-540-58085-9 75
48. Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Computer Aided
Verification, 20th International Conference, CAV 2008. pp. 162–175 (2008), https:
//doi.org/10.1007/978-3-540-70545-1 16