---
_id: '5549'
abstract:
- lang: eng
  text: "This repository contains the experimental part of the CAV 2015 publication
    Counterexample Explanation by Learning Small Strategies in Markov Decision Processes.\r\nWe
    extended the probabilistic model checker PRISM to represent strategies of Markov
    Decision Processes as Decision Trees.\r\nThe archive contains a java executable
    version of the extended tool (prism_dectree.jar) together with a few examples
    of the PRISM benchmark library.\r\nTo execute the program, please have a look
    at the README.txt, which provides instructions and further information on the
    archive.\r\nThe archive contains scripts that (if run often enough) reproduces
    the data presented in the publication."
article_processing_charge: No
author:
- first_name: Andreas
  full_name: Fellner, Andreas
  id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
  last_name: Fellner
citation:
  ama: 'Fellner A. Experimental part of CAV 2015 publication: Counterexample Explanation
    by Learning Small Strategies in Markov Decision Processes. 2015. doi:<a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>'
  apa: 'Fellner, A. (2015). Experimental part of CAV 2015 publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes. Institute
    of Science and Technology Austria. <a href="https://doi.org/10.15479/AT:ISTA:28">https://doi.org/10.15479/AT:ISTA:28</a>'
  chicago: 'Fellner, Andreas. “Experimental Part of CAV 2015 Publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes.” Institute
    of Science and Technology Austria, 2015. <a href="https://doi.org/10.15479/AT:ISTA:28">https://doi.org/10.15479/AT:ISTA:28</a>.'
  ieee: 'A. Fellner, “Experimental part of CAV 2015 publication: Counterexample Explanation
    by Learning Small Strategies in Markov Decision Processes.” Institute of Science
    and Technology Austria, 2015.'
  ista: 'Fellner A. 2015. Experimental part of CAV 2015 publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes, Institute
    of Science and Technology Austria, <a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>.'
  mla: 'Fellner, Andreas. <i>Experimental Part of CAV 2015 Publication: Counterexample
    Explanation by Learning Small Strategies in Markov Decision Processes</i>. Institute
    of Science and Technology Austria, 2015, doi:<a href="https://doi.org/10.15479/AT:ISTA:28">10.15479/AT:ISTA:28</a>.'
  short: A. Fellner, (2015).
contributor:
- first_name: Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
datarep_id: '28'
date_created: 2018-12-12T12:31:29Z
date_published: 2015-08-13T00:00:00Z
date_updated: 2024-02-21T13:52:07Z
day: '13'
ddc:
- '004'
department:
- _id: KrCh
- _id: ToHe
doi: 10.15479/AT:ISTA:28
ec_funded: 1
file:
- access_level: open_access
  checksum: b8bcb43c0893023cda66c1b69c16ac62
  content_type: application/zip
  creator: system
  date_created: 2018-12-12T13:02:31Z
  date_updated: 2020-07-14T12:47:00Z
  file_id: '5597'
  file_name: IST-2015-28-v1+2_Fellner_DataRep.zip
  file_size: 49557109
  relation: main_file
file_date_updated: 2020-07-14T12:47:00Z
has_accepted_license: '1'
keyword:
- Markov Decision Process
- Decision Tree
- Probabilistic Verification
- Counterexample Explanation
license: https://creativecommons.org/publicdomain/zero/1.0/
month: '08'
oa: 1
oa_version: Published Version
project:
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publisher: Institute of Science and Technology Austria
publist_id: '5564'
related_material:
  record:
  - id: '1603'
    relation: popular_science
    status: public
status: public
title: 'Experimental part of CAV 2015 publication: Counterexample Explanation by Learning
  Small Strategies in Markov Decision Processes'
tmp:
  image: /images/cc_0.png
  legal_code_url: https://creativecommons.org/publicdomain/zero/1.0/legalcode
  name: Creative Commons Public Domain Dedication (CC0 1.0)
  short: CC0 (1.0)
type: research_data
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2015'
...
---
_id: '1603'
abstract:
- lang: eng
  text: "For deterministic systems, a counterexample to a property can simply be an
    error trace, whereas counterexamples in probabilistic systems are necessarily
    more complex. For instance, a set of erroneous traces with a sufficient cumulative
    probability mass can be used. Since these are too large objects to understand
    and manipulate, compact representations such as subchains have been considered.
    In the case of probabilistic systems with non-determinism, the situation is even
    more complex. While a subchain for a given strategy (or scheduler, resolving non-determinism)
    is a straightforward choice, we take a different approach. Instead, we focus on
    the strategy itself, and extract the most important decisions it makes, and present
    its succinct representation.\r\nThe key tools we employ to achieve this are (1)
    introducing a concept of importance of a state w.r.t. the strategy, and (2) learning
    using decision trees. There are three main consequent advantages of our approach.
    Firstly, it exploits the quantitative information on states, stressing the more
    important decisions. Secondly, it leads to a greater variability and degree of
    freedom in representing the strategies. Thirdly, the representation uses a self-explanatory
    data structure. In summary, our approach produces more succinct and more explainable
    strategies, as opposed to e.g. binary decision diagrams. Finally, our experimental
    results show that we can extract several rules describing the strategy even for
    very large systems that do not fit in memory, and based on the rules explain the
    erroneous behaviour."
acknowledgement: This research was funded in part by Austrian Science Fund (FWF) Grant
  No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE) and Z211-N23 (Wittgenstein Award),
  European Research Council (ERC) Grant No 279307 (Graph Games), ERC Grant No 267989
  (QUAREM), the Czech Science Foundation Grant No P202/12/G061, and People Programme
  (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007–2013)
  REA Grant No 291734.
alternative_title:
- LNCS
author:
- first_name: Tomáš
  full_name: Brázdil, Tomáš
  last_name: Brázdil
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Martin
  full_name: Chmelik, Martin
  id: 3624234E-F248-11E8-B48F-1D18A9856A87
  last_name: Chmelik
- first_name: Andreas
  full_name: Fellner, Andreas
  id: 42BABFB4-F248-11E8-B48F-1D18A9856A87
  last_name: Fellner
- first_name: Jan
  full_name: Kretinsky, Jan
  id: 44CEF464-F248-11E8-B48F-1D18A9856A87
  last_name: Kretinsky
  orcid: 0000-0002-8122-2881
citation:
  ama: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample
    explanation by learning small strategies in Markov decision processes. In: Vol
    9206. Springer; 2015:158-177. doi:<a href="https://doi.org/10.1007/978-3-319-21690-4_10">10.1007/978-3-319-21690-4_10</a>'
  apa: 'Brázdil, T., Chatterjee, K., Chmelik, M., Fellner, A., &#38; Kretinsky, J.
    (2015). Counterexample explanation by learning small strategies in Markov decision
    processes (Vol. 9206, pp. 158–177). Presented at the CAV: Computer Aided Verification,
    San Francisco, CA, United States: Springer. <a href="https://doi.org/10.1007/978-3-319-21690-4_10">https://doi.org/10.1007/978-3-319-21690-4_10</a>'
  chicago: Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Andreas Fellner,
    and Jan Kretinsky. “Counterexample Explanation by Learning Small Strategies in
    Markov Decision Processes,” 9206:158–77. Springer, 2015. <a href="https://doi.org/10.1007/978-3-319-21690-4_10">https://doi.org/10.1007/978-3-319-21690-4_10</a>.
  ieee: 'T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, and J. Kretinsky, “Counterexample
    explanation by learning small strategies in Markov decision processes,” presented
    at the CAV: Computer Aided Verification, San Francisco, CA, United States, 2015,
    vol. 9206, pp. 158–177.'
  ista: 'Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. 2015. Counterexample
    explanation by learning small strategies in Markov decision processes. CAV: Computer
    Aided Verification, LNCS, vol. 9206, 158–177.'
  mla: Brázdil, Tomáš, et al. <i>Counterexample Explanation by Learning Small Strategies
    in Markov Decision Processes</i>. Vol. 9206, Springer, 2015, pp. 158–77, doi:<a
    href="https://doi.org/10.1007/978-3-319-21690-4_10">10.1007/978-3-319-21690-4_10</a>.
  short: T. Brázdil, K. Chatterjee, M. Chmelik, A. Fellner, J. Kretinsky, in:, Springer,
    2015, pp. 158–177.
conference:
  end_date: 2015-07-24
  location: San Francisco, CA, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2015-07-18
date_created: 2018-12-11T11:52:58Z
date_published: 2015-07-16T00:00:00Z
date_updated: 2024-02-21T13:52:07Z
day: '16'
department:
- _id: KrCh
- _id: ToHe
doi: 10.1007/978-3-319-21690-4_10
ec_funded: 1
intvolume: '      9206'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: http://arxiv.org/abs/1502.02834
month: '07'
oa: 1
oa_version: Preprint
page: 158 - 177
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: P 23499-N23
  name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '279307'
  name: 'Quantitative Graph Games: Theory and Applications'
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25681D80-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '291734'
  name: International IST Postdoc Fellowship Programme
publication_identifier:
  eisbn:
  - 978-3-319-21690-4
publication_status: published
publisher: Springer
publist_id: '5564'
quality_controlled: '1'
related_material:
  record:
  - id: '5549'
    relation: research_paper
    status: public
scopus_import: 1
status: public
title: Counterexample explanation by learning small strategies in Markov decision
  processes
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9206
year: '2015'
...