340
F. Funke et al.
References
1. ´
Abrah´ am, 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–121 (2014),
https://doi.org/10.1007/978-3-319-07317-0 3
2. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford
University, Department of Computer Science (1997)
3. de Alfaro, L.: Temporal logics for the specification of performance and reliability.
In: STACS 97. pp. 165–176. Springer, Berlin, Heidelberg (1997)
4. 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–187 (2011), https://doi.org/10.1007/
978-3-642-22306-8 13
5. 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–51 (2006), https://doi.org/10.1007/11867340 4
6. 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–206 (2009), https://doi.org/10.1109/QEST.2009.10
7. 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–60 (2010), https://doi.org/10.1109/TSE.2009.57
8. Amaldi, E., Kann, V.: On the approximability of minimizing nonzero variables or
unsatisfied relations in linear systems. Theoretical Computer Science 209(1), 237 –
260 (1998), http://www.sciencedirect.com/science/article/pii/S0304397597001151
9. Andr´ es, M.E., D’Argenio, 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–148
(2008), https://doi.org/10.1007/978-3-642-01702-5 15
10. Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of
Algorithms 11(3), 441–461 (1990), https://doi.org/10.1016/0196-6774(90)90021-6
11. Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration
of arrangements and polyhedra. Discrete & Computational Geometry 8, 295–313
(1992), https://doi.org/10.1007/BF02293050
12. Avis, D., Fukuda, K.: Reverse search for enumeration. Discrete Applied Mathematics
65, 21–46 (1993)
13. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind
Series). The MIT Press, Cambridge, MA (2008)
14. 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–88 (1961),
https://doi.org/10.1137/0109008
15. 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–69 (2017),
https://doi.org/10.1007/978-3-319-66197-1 4
16. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic
systems. In: Foundations of Software Technology and Theoretical Computer Science.
pp. 499–513. Springer, Berlin, Heidelberg (1995)
F. Funke et al.
References
1. ´
Abrah´ am, 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–121 (2014),
https://doi.org/10.1007/978-3-319-07317-0 3
2. de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford
University, Department of Computer Science (1997)
3. de Alfaro, L.: Temporal logics for the specification of performance and reliability.
In: STACS 97. pp. 165–176. Springer, Berlin, Heidelberg (1997)
4. 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–187 (2011), https://doi.org/10.1007/
978-3-642-22306-8 13
5. 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–51 (2006), https://doi.org/10.1007/11867340 4
6. 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–206 (2009), https://doi.org/10.1109/QEST.2009.10
7. 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–60 (2010), https://doi.org/10.1109/TSE.2009.57
8. Amaldi, E., Kann, V.: On the approximability of minimizing nonzero variables or
unsatisfied relations in linear systems. Theoretical Computer Science 209(1), 237 –
260 (1998), http://www.sciencedirect.com/science/article/pii/S0304397597001151
9. Andr´ es, M.E., D’Argenio, 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–148
(2008), https://doi.org/10.1007/978-3-642-01702-5 15
10. Aspnes, J., Herlihy, M.: Fast randomized consensus using shared memory. Journal of
Algorithms 11(3), 441–461 (1990), https://doi.org/10.1016/0196-6774(90)90021-6
11. Avis, D., Fukuda, K.: A pivoting algorithm for convex hulls and vertex enumeration
of arrangements and polyhedra. Discrete & Computational Geometry 8, 295–313
(1992), https://doi.org/10.1007/BF02293050
12. Avis, D., Fukuda, K.: Reverse search for enumeration. Discrete Applied Mathematics
65, 21–46 (1993)
13. Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind
Series). The MIT Press, Cambridge, MA (2008)
14. 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–88 (1961),
https://doi.org/10.1137/0109008
15. 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–69 (2017),
https://doi.org/10.1007/978-3-319-66197-1 4
16. Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic
systems. In: Foundations of Software Technology and Theoretical Computer Science.
pp. 499–513. Springer, Berlin, Heidelberg (1995)
