Farkas certificates and minimal witnesses
343
49. Jansen, N., ´
Abrah´ am, 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–452 (2011), https://doi.org/10.1007/978-3-642-24372-1 33
50. Jansen, N., ´
Abrah´ am, 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–353 (2012), https://doi.org/10.1007/978-3-642-33386-6 27
51. Jansen, N., ´
Abrah´ am, 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–151 (2012), https://doi.org/10.1007/978-3-642-35861-6 9
52. Jansen, N., Wimmer, R., ´
Abrah´ am, E., Zajzon, B., Katoen, J., Becker, B., Schuster,
J.: Symbolic counterexample generation for large discrete-time Markov chains.
Science of Computer Programming 91, 90–114 (2014), https://doi.org/10.1016/j.
scico.2014.02.001
53. 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–190 (2019), https://doi.org/10.
1007/978-3-030-17465-1 10
54. 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–103. Springer US, Boston, MA (1972)
55. Khachiyan, L., Boros, E., Borys, K., Elbassioni, K., Gurvich, V.: Generating all
vertices of a polyhedron is hard. Discrete & Computational Geometry 39(1), 174–190
(2008), https://doi.org/10.1007/s00454-008-9050-5
56. 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–84 (2011),
https://doi.org/10.1007/978-3-642-24270-0 6
57. 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–606 (2004), https://doi.org/10.1007/
978-3-540-24730-2 43
58. 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–591 (2011), https://doi.org/10.1007/978-3-642-22110-1 47
59. Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In:
Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012.
pp. 203–204 (2012), https://doi.org/10.1109/QEST.2012.14
60. 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–206 (2001),
https://doi.org/10.1007/3-540-44585-4 17
61. Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking
for probabilistic timed automata. Information and Computation 205(7), 1027–1077
(2007), https://doi.org/10.1016/j.ic.2007.01.004
62. Mangasarian, O.: Nonlinear Programming. Classics in Applied Mathematics, Society
for Industrial and Applied Mathematics (1994)
343
49. Jansen, N., ´
Abrah´ am, 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–452 (2011), https://doi.org/10.1007/978-3-642-24372-1 33
50. Jansen, N., ´
Abrah´ am, 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–353 (2012), https://doi.org/10.1007/978-3-642-33386-6 27
51. Jansen, N., ´
Abrah´ am, 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–151 (2012), https://doi.org/10.1007/978-3-642-35861-6 9
52. Jansen, N., Wimmer, R., ´
Abrah´ am, E., Zajzon, B., Katoen, J., Becker, B., Schuster,
J.: Symbolic counterexample generation for large discrete-time Markov chains.
Science of Computer Programming 91, 90–114 (2014), https://doi.org/10.1016/j.
scico.2014.02.001
53. 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–190 (2019), https://doi.org/10.
1007/978-3-030-17465-1 10
54. 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–103. Springer US, Boston, MA (1972)
55. Khachiyan, L., Boros, E., Borys, K., Elbassioni, K., Gurvich, V.: Generating all
vertices of a polyhedron is hard. Discrete & Computational Geometry 39(1), 174–190
(2008), https://doi.org/10.1007/s00454-008-9050-5
56. 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–84 (2011),
https://doi.org/10.1007/978-3-642-24270-0 6
57. 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–606 (2004), https://doi.org/10.1007/
978-3-540-24730-2 43
58. 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–591 (2011), https://doi.org/10.1007/978-3-642-22110-1 47
59. Kwiatkowska, M.Z., Norman, G., Parker, D.: The PRISM benchmark suite. In:
Ninth International Conference on Quantitative Evaluation of Systems, QEST 2012.
pp. 203–204 (2012), https://doi.org/10.1109/QEST.2012.14
60. 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–206 (2001),
https://doi.org/10.1007/3-540-44585-4 17
61. Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking
for probabilistic timed automata. Information and Computation 205(7), 1027–1077
(2007), https://doi.org/10.1016/j.ic.2007.01.004
62. Mangasarian, O.: Nonlinear Programming. Classics in Applied Mathematics, Society
for Industrial and Applied Mathematics (1994)