[{"status":"public","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"name":"Security and Privacy by Design for Complex Systems","grant_number":"F8512","_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f"}],"doi":"10.15479/AT-ISTA-21401","date_published":"2026-03-05T00:00:00Z","ddc":["000"],"citation":{"apa":"Karimi, M. (2026). <i>Privacy-preserving runtime verification</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>","mla":"Karimi, Mahyar. <i>Privacy-Preserving Runtime Verification</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>.","chicago":"Karimi, Mahyar. “Privacy-Preserving Runtime Verification.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>.","ista":"Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science and Technology Austria.","ama":"Karimi M. Privacy-preserving runtime verification. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>","short":"M. Karimi, Privacy-Preserving Runtime Verification, Institute of Science and Technology Austria, 2026.","ieee":"M. Karimi, “Privacy-preserving runtime verification,” Institute of Science and Technology Austria, 2026."},"oa_version":"Published Version","type":"dissertation","month":"03","related_material":{"record":[{"id":"21020","status":"public","relation":"part_of_dissertation"}]},"abstract":[{"text":"Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.\r\n\r\nIn this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation.\r\n\r\nThe sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.\r\n","lang":"eng"}],"keyword":["Privacy-preserving verification","Runtime verification","Monitoring","Reactive functionalities","Cryptographic protocols"],"ec_funded":1,"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","publication_status":"published","fulldoi":"https://doi.org/10.15479/AT-ISTA-21401","date_updated":"2026-03-13T13:37:20Z","article_processing_charge":"No","has_accepted_license":"1","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"alternative_title":["ISTA Master’s Thesis"],"file_date_updated":"2026-03-10T15:20:09Z","_id":"21401","page":"60","date_created":"2026-03-05T15:20:47Z","title":"Privacy-preserving runtime verification","author":[{"last_name":"Karimi","full_name":"Karimi, Mahyar","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","orcid":"0009-0005-0820-1696","first_name":"Mahyar"}],"publication_identifier":{"issn":["2791-4585"]},"publisher":"Institute of Science and Technology Austria","file":[{"file_size":766048,"content_type":"application/pdf","date_created":"2026-03-06T14:06:25Z","date_updated":"2026-03-10T15:20:09Z","file_name":"2026_Karimi_Mahyar_Thesis.pdf","relation":"main_file","creator":"mkarimi","file_id":"21404","access_level":"open_access","checksum":"3f49f05c9d123e14d7adb73d3bc50fe2"},{"content_type":"application/zip","file_name":"2026_Karimi_Mahyar_Thesis_src.zip","date_created":"2026-03-06T14:06:25Z","date_updated":"2026-03-06T14:06:25Z","file_size":1243394,"file_id":"21405","access_level":"closed","relation":"source_file","creator":"mkarimi","checksum":"8fb9db4b4187e26443369a993427a5ff"}],"acknowledgement":"This work is part of the project VAMOS, which has received funding from the European\r\nResearch Council (ERC) under grant agreement No. 101020093, and the Austrian Science\r\nFund (FWF) SFB project SpyCoDe F8502.\r\n","degree_awarded":"MS","day":"05","supervisor":[{"first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"oa":1,"year":"2026","corr_author":"1","OA_place":"repository","language":[{"iso":"eng"}]},{"status":"public","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"OA_type":"gold","dataavailabilitystatement":"Software (Source Code): https://github.com/filipcano/monitoringdiscounted-sum-properties [10]\r\narchived at swh:1:dir:cb99396415f279c985cd05206b44320227f64245\r\n","doi":"10.4230/LIPIcs.CONCUR.2026.22","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","image":"/images/cc_by.png"},"date_published":"2026-08-24T00:00:00Z","ddc":["000"],"citation":{"ista":"Cano Cordoba F, Henzinger TA, Kueffner K, Sarac NE. 2026. Monitoring discounted sum properties. 37th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 391, 22:1-22:19.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, Konstantin Kueffner, and Naci E Sarac. “Monitoring Discounted Sum Properties.” In <i>37th International Conference on Concurrency Theory</i>, Vol. 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.22</a>.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K, Sarac NE. Monitoring discounted sum properties. In: <i>37th International Conference on Concurrency Theory</i>. Vol 391. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22\">10.4230/LIPIcs.CONCUR.2026.22</a>","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, N.E. Sarac, in:, 37th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","ieee":"F. Cano Cordoba, T. A. Henzinger, K. Kueffner, and N. E. Sarac, “Monitoring discounted sum properties,” in <i>37th International Conference on Concurrency Theory</i>, Liverpool, United Kingdom, 2026, vol. 391.","apa":"Cano Cordoba, F., Henzinger, T. A., Kueffner, K., &#38; Sarac, N. E. (2026). Monitoring discounted sum properties. In <i>37th International Conference on Concurrency Theory</i> (Vol. 391). Liverpool, United Kingdom: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22\">https://doi.org/10.4230/LIPIcs.CONCUR.2026.22</a>","mla":"Cano Cordoba, Filip, et al. “Monitoring Discounted Sum Properties.” <i>37th International Conference on Concurrency Theory</i>, vol. 391, 22:1-22:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22\">10.4230/LIPIcs.CONCUR.2026.22</a>."},"oa_version":"Published Version","das_tickbox":"1","external_id":{"arxiv":["2606.25979"]},"type":"conference","month":"08","abstract":[{"text":"Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obscure local structure. Localisation measures such as discounted averages offer a principled middle ground, yet remain poorly understood in runtime verification. This paper studies discounted sums from a monitoring perspective, in both deterministic and stochastic settings. We formalize the discounted monitoring problem and show that exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce ε-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We then extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform (ε,δ)-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We also formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. Finally, we present a specification language for arithmetic expressions over multiple discounted sums with synchronous and asynchronous semantics, and evaluate our approach on practical scenarios including algorithmic fairness.","lang":"eng"}],"keyword":["Runtime Verification","Probabilistic Systems","Quantitative Verification","Approximate Monitoring"],"researchdata_availability":"no","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ec_funded":1,"date_updated":"2026-09-22T06:02:06Z","fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2026.22","publication_status":"published","has_accepted_license":"1","article_processing_charge":"Yes","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"alternative_title":["LIPIcs"],"license":"https://creativecommons.org/licenses/by/4.0/","article_number":"22:1-22:19","supplementarymaterial":"no","date_created":"2026-09-13T22:01:54Z","_id":"22921","file_date_updated":"2026-09-22T05:59:03Z","quality_controlled":"1","title":"Monitoring discounted sum properties","author":[{"full_name":"Cano Cordoba, Filip","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","first_name":"Filip","orcid":"0000-0002-0783-904X"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"orcid":"0000-0001-8974-2542","first_name":"Konstantin","full_name":"Kueffner, Konstantin","last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E","first_name":"Naci E"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959774475"]},"scopus_import":"1","file":[{"relation":"main_file","creator":"dernst","access_level":"open_access","file_id":"22978","checksum":"f7b2e22428344fd7972c54f099df6aba","success":1,"file_size":997156,"file_name":"2026_LIPIcsCONCUR_Cano.pdf","date_updated":"2026-09-22T05:59:03Z","date_created":"2026-09-22T05:59:03Z","content_type":"application/pdf"}],"arxiv":1,"day":"24","acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC2020-AdG 101020093 and ERC-2021-AdG 101055412.\r\nFilip Cano: ERC-2020-AdG 101020093\r\nThomas A. Henzinger: ERC-2020-AdG 101020093\r\nKonstantin Kueffner: ERC-2020-AdG 101020093\r\nN. Ege Saraç: ERC-2021-AdG 101055412","volume":391,"publication":"37th International Conference on Concurrency Theory","oa":1,"conference":{"name":"CONCUR: Conference on Concurrency Theory","location":"Liverpool, United Kingdom","end_date":"2026-09-04","start_date":"2026-09-01"},"intvolume":"       391","year":"2026","language":[{"iso":"eng"}],"corr_author":"1","OA_place":"publisher"},{"quality_controlled":"1","title":"Off-the-Shelf cooperative software verification by splitting programs dynamically","author":[{"last_name":"Richter","full_name":"Richter, Cedric","first_name":"Cedric"},{"full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek"},{"first_name":"Marie Christine","last_name":"Jakobs","full_name":"Jakobs, Marie Christine"},{"last_name":"Wehrheim","full_name":"Wehrheim, Heike","first_name":"Heike"}],"publisher":"Gesellschaft für Informatik","publication_identifier":{"eissn":["1617-5468"]},"scopus_import":"1","file":[{"file_name":"2026_LNI_Richter.pdf","date_updated":"2026-10-19T08:39:37Z","date_created":"2026-10-19T08:39:37Z","content_type":"application/pdf","file_size":147208,"checksum":"3371c63711ed26efa41744834d337d28","success":1,"access_level":"open_access","file_id":"23170","relation":"main_file","creator":"dernst"}],"supplementarymaterial":"no","_id":"22622","date_created":"2026-08-02T22:01:54Z","page":"41-42","file_date_updated":"2026-10-19T08:39:37Z","oa":1,"conference":{"end_date":"2026-02-27","start_date":"2026-02-23","name":"SE: Software Engineering","location":"Bonn, Switzerland"},"year":"2026","language":[{"iso":"eng"}],"OA_place":"publisher","day":"01","volume":"P-377","publication":"Software Engineering 2026","oa_version":"Published Version","das_tickbox":"1","type":"conference","month":"03","abstract":[{"text":"Cooperative software verification aims at improving the effectiveness and efficiency of software verification by enabling multiple verification tools to work together. Existing cooperative verification schemes, however, typically require specialized interfaces or tight integration, limiting their practical applicability. In our International Conference on Software Engineering (ICSE) 2025 publication, we introduce dynamic program splitting – a novel approach that enables cooperation between off-the-shelf verification tools without requiring any modifications. The key idea is to probe verification tools on a given verification task under a time limit and split tasks dynamically that cannot be verified under the given time constraints. The process continues recursively, incrementally identifying program parts that are particularly hard for the given verifier. The remaining unverified parts are provided to a second verifier, allowing to leverage the complementary strengths of different tools. Our evaluation on SV-COMP benchmarks demonstrates that cooperation through dynamic program splitting enables the verification of tasks that none of the individual verifiers can solve on their own.","lang":"eng"}],"status":"public","OA_type":"hybrid","doi":"10.18420/se2026_45","dataavailabilitystatement":"All our implementations and data are archived and available at Zenodo5\r\nand are evaluated as an artifact in the ICSE 2025 artifact evaluation. Furthermore, our\r\napproach is integrated into the software verifier Bubaak [CR25] which we submitted as\r\npart of our contribution to SV-COMP 2025.","date_published":"2026-03-01T00:00:00Z","tmp":{"image":"/images/cc_by_sa.png","legal_code_url":"https://creativecommons.org/licenses/by-sa/4.0/legalcode","name":"Creative Commons Attribution-ShareAlike 4.0 International Public License (CC BY-SA 4.0)","short":"CC BY-SA (4.0)"},"citation":{"ista":"Richter C, Chalupa M, Jakobs MC, Wehrheim H. 2026. Off-the-Shelf cooperative software verification by splitting programs dynamically. Software Engineering 2026. SE: Software Engineering, Lecture Notes in Informatics, vol. P-377, 41–42.","chicago":"Richter, Cedric, Marek Chalupa, Marie Christine Jakobs, and Heike Wehrheim. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” In <i>Software Engineering 2026</i>, P-377:41–42. Gesellschaft für Informatik, 2026. <a href=\"https://doi.org/10.18420/se2026_45\">https://doi.org/10.18420/se2026_45</a>.","ama":"Richter C, Chalupa M, Jakobs MC, Wehrheim H. Off-the-Shelf cooperative software verification by splitting programs dynamically. In: <i>Software Engineering 2026</i>. Vol P-377. Gesellschaft für Informatik; 2026:41-42. doi:<a href=\"https://doi.org/10.18420/se2026_45\">10.18420/se2026_45</a>","short":"C. Richter, M. Chalupa, M.C. Jakobs, H. Wehrheim, in:, Software Engineering 2026, Gesellschaft für Informatik, 2026, pp. 41–42.","ieee":"C. Richter, M. Chalupa, M. C. Jakobs, and H. Wehrheim, “Off-the-Shelf cooperative software verification by splitting programs dynamically,” in <i>Software Engineering 2026</i>, Bonn, Switzerland, 2026, vol. P-377, pp. 41–42.","apa":"Richter, C., Chalupa, M., Jakobs, M. C., &#38; Wehrheim, H. (2026). Off-the-Shelf cooperative software verification by splitting programs dynamically. In <i>Software Engineering 2026</i> (Vol. P-377, pp. 41–42). Bonn, Switzerland: Gesellschaft für Informatik. <a href=\"https://doi.org/10.18420/se2026_45\">https://doi.org/10.18420/se2026_45</a>","mla":"Richter, Cedric, et al. “Off-the-Shelf Cooperative Software Verification by Splitting Programs Dynamically.” <i>Software Engineering 2026</i>, vol. P-377, Gesellschaft für Informatik, 2026, pp. 41–42, doi:<a href=\"https://doi.org/10.18420/se2026_45\">10.18420/se2026_45</a>."},"ddc":["000"],"has_accepted_license":"1","article_processing_charge":"No","alternative_title":["Lecture Notes in Informatics"],"department":[{"_id":"ToHe"}],"license":"https://creativecommons.org/licenses/by-sa/4.0/","keyword":["Software Verification","Cooperation","Program Decomposition"],"researchdata_availability":"yes","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-10-19T08:49:32Z","fulldoi":"https://doi.org/10.18420/se2026_45","publication_status":"published"},{"date_created":"2022-05-12T07:14:01Z","_id":"11362","page":"124","file_date_updated":"2022-05-17T15:19:39Z","publisher":"Institute of Science and Technology Austria","publication_identifier":{"isbn":["978-3-99078-017-6"]},"file":[{"date_updated":"2022-05-13T12:49:00Z","file_name":"src.zip","date_created":"2022-05-13T12:33:26Z","content_type":"application/zip","file_size":13210143,"checksum":"8eefa9c7c10ca7e1a2ccdd731962a645","access_level":"closed","file_id":"11378","relation":"source_file","creator":"mlechner"},{"file_name":"thesis_main-a2.pdf","date_created":"2022-05-16T08:02:28Z","date_updated":"2022-05-17T15:19:39Z","content_type":"application/pdf","file_size":2732536,"access_level":"open_access","file_id":"11382","relation":"main_file","creator":"mlechner","checksum":"1b9e1e5a9a83ed9d89dad2f5133dc026"}],"title":"Learning verifiable representations","author":[{"full_name":"Lechner, Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","first_name":"Mathias"}],"day":"12","degree_awarded":"PhD","year":"2022","language":[{"iso":"eng"}],"corr_author":"1","OA_place":"publisher","oa":1,"supervisor":[{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"tmp":{"short":"CC BY-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nd/4.0/legalcode","name":"Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0)","image":"/image/cc_by_nd.png"},"date_published":"2022-05-12T00:00:00Z","ddc":["004"],"citation":{"chicago":"Lechner, Mathias. “Learning Verifiable Representations.” Institute of Science and Technology Austria, 2022. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>.","ama":"Lechner M. Learning verifiable representations. 2022. doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>","ista":"Lechner M. 2022. Learning verifiable representations. Institute of Science and Technology Austria.","short":"M. Lechner, Learning Verifiable Representations, Institute of Science and Technology Austria, 2022.","ieee":"M. Lechner, “Learning verifiable representations,” Institute of Science and Technology Austria, 2022.","mla":"Lechner, Mathias. <i>Learning Verifiable Representations</i>. Institute of Science and Technology Austria, 2022, doi:<a href=\"https://doi.org/10.15479/at:ista:11362\">10.15479/at:ista:11362</a>.","apa":"Lechner, M. (2022). <i>Learning verifiable representations</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:11362\">https://doi.org/10.15479/at:ista:11362</a>"},"project":[{"name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"status":"public","doi":"10.15479/at:ista:11362","month":"05","abstract":[{"lang":"eng","text":"Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks.\r\nOne exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. \r\nTo deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. \r\nThis can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks.\r\n\r\nOur goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications.\r\nThis thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making.\r\n\r\nFirst, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry.\r\nWe show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization.\r\n\r\nFurthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable.\r\nOur results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice.\r\n\r\nFinally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic.\r\nWe introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only.\r\nOur method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system.\r\nWe demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks."}],"related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"11366"},{"id":"7808","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","status":"public","id":"10666"},{"relation":"part_of_dissertation","id":"10667","status":"public"},{"relation":"part_of_dissertation","status":"public","id":"10665"}]},"oa_version":"Published Version","type":"dissertation","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","ec_funded":1,"fulldoi":"https://doi.org/10.15479/at:ista:11362","date_updated":"2026-08-19T09:28:05Z","publication_status":"published","keyword":["neural networks","verification","machine learning"],"license":"https://creativecommons.org/licenses/by-nd/4.0/","has_accepted_license":"1","article_processing_charge":"No","alternative_title":["ISTA Thesis"],"department":[{"_id":"GradSch"},{"_id":"ToHe"}]},{"publication":"International Conference on Runtime Verification","volume":12974,"acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Mae Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","day":"06","corr_author":"1","place":"Cham","language":[{"iso":"eng"}],"year":"2021","intvolume":"     12974","conference":{"location":"Virtual","name":"RV: Runtime Verification","end_date":"2021-10-14","start_date":"2021-10-11"},"oa":1,"file_date_updated":"2021-10-07T23:32:18Z","date_created":"2021-10-07T23:30:10Z","_id":"10108","page":"231-243","file":[{"file_size":350632,"file_name":"differentialmonitoring-cameraready-openaccess.pdf","date_updated":"2021-10-07T23:32:18Z","date_created":"2021-10-07T23:32:18Z","content_type":"application/pdf","checksum":"554c7fdb259eda703a8b6328a6dad55a","success":1,"relation":"main_file","creator":"fmuehlbo","access_level":"open_access","file_id":"10109"}],"scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["978-3-030-88494-9"],"isbn":["978-3-030-88493-2"]},"publisher":"Springer Nature","author":[{"last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","full_name":"Mühlböck, Fabian","first_name":"Fabian","orcid":"0000-0003-1548-0177"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"title":"Differential monitoring","quality_controlled":"1","publication_status":"published","date_updated":"2025-04-15T06:26:12Z","fulldoi":"https://doi.org/10.1007/978-3-030-88494-9_12","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","keyword":["run-time verification","software engineering","implicit specification"],"department":[{"_id":"ToHe"}],"alternative_title":["LNCS"],"article_processing_charge":"No","has_accepted_license":"1","ddc":["005"],"citation":{"ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring. International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 231–243.","ama":"Mühlböck F, Henzinger TA. Differential monitoring. In: <i>International Conference on Runtime Verification</i>. Vol 12974. Cham: Springer Nature; 2021:231-243. doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. “Differential Monitoring.” In <i>International Conference on Runtime Verification</i>, 12974:231–43. Cham: Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>.","ieee":"F. Mühlböck and T. A. Henzinger, “Differential monitoring,” in <i>International Conference on Runtime Verification</i>, Virtual, 2021, vol. 12974, pp. 231–243.","short":"F. Mühlböck, T.A. Henzinger, in:, International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 231–243.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). Differential monitoring. In <i>International Conference on Runtime Verification</i> (Vol. 12974, pp. 231–243). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">https://doi.org/10.1007/978-3-030-88494-9_12</a>","mla":"Mühlböck, Fabian, and Thomas A. Henzinger. “Differential Monitoring.” <i>International Conference on Runtime Verification</i>, vol. 12974, Springer Nature, 2021, pp. 231–43, doi:<a href=\"https://doi.org/10.1007/978-3-030-88494-9_12\">10.1007/978-3-030-88494-9_12</a>."},"date_published":"2021-10-06T00:00:00Z","doi":"10.1007/978-3-030-88494-9_12","isi":1,"status":"public","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"related_material":{"record":[{"status":"public","id":"9946","relation":"extended_version"}]},"abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"month":"10","external_id":{"isi":["000719383800012"]},"type":"conference","oa_version":"Preprint"},{"day":"31","degree_awarded":"PhD","oa":1,"supervisor":[{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"language":[{"iso":"eng"}],"corr_author":"1","OA_place":"publisher","acknowledged_ssus":[{"_id":"SSU"}],"year":"2021","date_created":"2021-10-29T20:09:01Z","_id":"10199","page":"166","file_date_updated":"2021-11-09T09:00:50Z","author":[{"first_name":"Viktor","orcid":"0000-0001-9036-063X","id":"3AF3DA7C-F248-11E8-B48F-1D18A9856A87","last_name":"Toman","full_name":"Toman, Viktor"}],"title":"Improved verification techniques for concurrent systems","file":[{"file_size":2915234,"content_type":"application/pdf","file_name":"toman_th_final.pdf","date_updated":"2021-11-08T14:12:22Z","date_created":"2021-11-08T14:12:22Z","checksum":"4f412a1ee60952221b499a4b1268df35","creator":"vtoman","relation":"main_file","file_id":"10225","access_level":"open_access"},{"content_type":"application/zip","file_name":"toman_thesis.zip","date_created":"2021-11-08T14:12:46Z","date_updated":"2021-11-09T09:00:50Z","file_size":8616056,"file_id":"10226","access_level":"closed","relation":"source_file","creator":"vtoman","checksum":"9584943f99127be2dd2963f6784c37d4"}],"publisher":"Institute of Science and Technology Austria","publication_identifier":{"issn":["2663-337X"]},"keyword":["concurrency","verification","model checking"],"date_updated":"2026-04-08T07:00:31Z","fulldoi":"https://doi.org/10.15479/at:ista:10199","publication_status":"published","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","ec_funded":1,"department":[{"_id":"GradSch"},{"_id":"KrCh"}],"alternative_title":["ISTA Thesis"],"has_accepted_license":"1","article_processing_charge":"No","doi":"10.15479/at:ista:10199","status":"public","project":[{"_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program","grant_number":"665385"},{"call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425","grant_number":"S11402-N23","name":"Rigorous Systems Engineering"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"citation":{"apa":"Toman, V. (2021). <i>Improved verification techniques for concurrent systems</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>","mla":"Toman, Viktor. <i>Improved Verification Techniques for Concurrent Systems</i>. Institute of Science and Technology Austria, 2021, doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>.","ieee":"V. Toman, “Improved verification techniques for concurrent systems,” Institute of Science and Technology Austria, 2021.","short":"V. Toman, Improved Verification Techniques for Concurrent Systems, Institute of Science and Technology Austria, 2021.","chicago":"Toman, Viktor. “Improved Verification Techniques for Concurrent Systems.” Institute of Science and Technology Austria, 2021. <a href=\"https://doi.org/10.15479/at:ista:10199\">https://doi.org/10.15479/at:ista:10199</a>.","ista":"Toman V. 2021. Improved verification techniques for concurrent systems. Institute of Science and Technology Austria.","ama":"Toman V. Improved verification techniques for concurrent systems. 2021. doi:<a href=\"https://doi.org/10.15479/at:ista:10199\">10.15479/at:ista:10199</a>"},"ddc":["000"],"date_published":"2021-10-31T00:00:00Z","type":"dissertation","oa_version":"Published Version","related_material":{"record":[{"status":"public","id":"9987","relation":"part_of_dissertation"},{"id":"10191","status":"public","relation":"part_of_dissertation"},{"relation":"part_of_dissertation","id":"141","status":"public"},{"relation":"part_of_dissertation","id":"10190","status":"public"}]},"abstract":[{"lang":"eng","text":"The design and verification of concurrent systems remains an open challenge due to the non-determinism that arises from the inter-process communication. In particular, concurrent programs are notoriously difficult both to be written correctly and to be analyzed formally, as complex thread interaction has to be accounted for. The difficulties are further exacerbated when concurrent programs get executed on modern-day hardware, which contains various buffering and caching mechanisms for efficiency reasons. This causes further subtle non-determinism, which can often produce very unintuitive behavior of the concurrent programs. Model checking is at the forefront of tackling the verification problem, where the task is to decide, given as input a concurrent system and a desired property, whether the system satisfies the property. The inherent state-space explosion problem in model checking of concurrent systems causes naïve explicit methods not to scale, thus more inventive methods are required. One such method is stateless model checking (SMC), which explores in memory-efficient manner the program executions rather than the states of the program. State-of-the-art SMC is typically coupled with partial order reduction (POR) techniques, which argue that certain executions provably produce identical system behavior, thus limiting the amount of executions one needs to explore in order to cover all possible behaviors. Another method to tackle the state-space explosion is symbolic model checking, where the considered techniques operate on a succinct implicit representation of the input system rather than explicitly accessing the system. In this thesis we present new techniques for verification of concurrent systems. We present several novel POR methods for SMC of concurrent programs under various models of semantics, some of which account for write-buffering mechanisms. Additionally, we present novel algorithms for symbolic model checking of finite-state concurrent systems, where the desired property of the systems is to ensure a formally defined notion of fairness."}],"month":"10"},{"has_accepted_license":"1","article_processing_charge":"No","alternative_title":["IST Austria Technical Report"],"department":[{"_id":"ToHe"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","fulldoi":"https://doi.org/10.15479/AT:ISTA:9946","date_updated":"2025-04-15T06:55:00Z","publication_status":"published","keyword":["run-time verification","software engineering","implicit specification"],"month":"09","abstract":[{"text":"We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.","lang":"eng"}],"related_material":{"record":[{"relation":"shorter_version","status":"public","id":"10108"},{"status":"public","id":"9281","relation":"other"}]},"oa_version":"Published Version","type":"technical_report","date_published":"2021-09-01T00:00:00Z","citation":{"mla":"Mühlböck, Fabian, and Thomas A. Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>.","apa":"Mühlböck, F., &#38; Henzinger, T. A. (2021). <i>Differential monitoring</i>. IST Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>","ama":"Mühlböck F, Henzinger TA. <i>Differential Monitoring</i>. IST Austria; 2021. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:9946\">10.15479/AT:ISTA:9946</a>","chicago":"Mühlböck, Fabian, and Thomas A Henzinger. <i>Differential Monitoring</i>. IST Austria, 2021. <a href=\"https://doi.org/10.15479/AT:ISTA:9946\">https://doi.org/10.15479/AT:ISTA:9946</a>.","ista":"Mühlböck F, Henzinger TA. 2021. Differential monitoring, IST Austria, 17p.","ieee":"F. Mühlböck and T. A. Henzinger, <i>Differential monitoring</i>. IST Austria, 2021.","short":"F. Mühlböck, T.A. Henzinger, Differential Monitoring, IST Austria, 2021."},"ddc":["005"],"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Formal methods for the design and analysis of complex systems","grant_number":"Z211"}],"status":"public","doi":"10.15479/AT:ISTA:9946","year":"2021","language":[{"iso":"eng"}],"oa":1,"day":"01","acknowledgement":"The authors would like to thank Borzoo Bonakdarpour, Derek Dreyer, Adrian Francalanza, Owolabi Legunsen, Matthew Milano, Manuel Rigger, Cesar Sanchez, and the members of the IST Verification Seminar for their helpful comments and insights on various stages of this work, as well as the reviewers of RV’21 for their helpful suggestions on the actual paper.","publisher":"IST Austria","publication_identifier":{"issn":["2664-1690"]},"file":[{"checksum":"0f9aafd59444cb6bdca6925d163ab946","creator":"fmuehlbo","relation":"main_file","file_id":"9948","access_level":"open_access","file_size":"320453","content_type":"application/pdf","date_updated":"2021-09-03T12:34:28Z","file_name":"differentialmonitoring-techreport.pdf","date_created":"2021-08-20T19:59:44Z"}],"title":"Differential monitoring","author":[{"orcid":"0000-0003-1548-0177","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","last_name":"Mühlböck","full_name":"Mühlböck, Fabian"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"}],"_id":"9946","date_created":"2021-08-20T20:00:37Z","page":"17","file_date_updated":"2021-09-03T12:34:28Z"},{"oa":1,"conference":{"end_date":"2021-07-02","start_date":"2021-06-29","location":"Rome, Italy","name":"LICS: Logic in Computer Science"},"language":[{"iso":"eng"}],"year":"2021","arxiv":1,"day":"07","acknowledgement":"The authors are grateful to the anonymous referees for their valuable comments. A. S. is fully supported by the Vienna Science and Technology Fund (WWTF) through project ICT15–003. K. C. is supported by the Austrian Science Fund (FWF) NFN Grant No S11407-N23 (RiSE/SHiNE) and by the ERC CoG 863818 (ForM-SMArt). For M. H. the research leading to these results has received funding from the European Research Council under the European Unions Seventh Framework Programme (FP/2007–2013) / ERC Grant Agreement no. 340506.","publication":"Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science","author":[{"first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Dvorak","full_name":"Dvorak, Wolfgang","first_name":"Wolfgang"},{"first_name":"Monika H","orcid":"0000-0002-5008-6530","full_name":"Henzinger, Monika H","id":"540c9bbd-f2de-11ec-812d-d04a5be85630","last_name":"Henzinger"},{"first_name":"Alexander","last_name":"Svozil","full_name":"Svozil, Alexander"}],"quality_controlled":"1","title":"Symbolic time and space tradeoffs for probabilistic verification","scopus_import":"1","publisher":"IEEE","publication_identifier":{"eisbn":["978-1-6654-4895-6"],"issn":["1043-6871"],"isbn":["978-1-6654-4896-3"]},"page":"1-13","_id":"10002","date_created":"2021-09-12T22:01:24Z","department":[{"_id":"KrCh"}],"article_processing_charge":"No","keyword":["Computer science","Computational modeling","Markov processes","Probabilistic logic","Formal verification","Game Theory"],"fulldoi":"https://doi.org/10.1109/LICS52264.2021.9470739","date_updated":"2026-08-12T06:39:42Z","publication_status":"published","ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","external_id":{"isi":["000947350400089"],"arxiv":["2104.07466"]},"oa_version":"Preprint","abstract":[{"lang":"eng","text":"We present a faster symbolic algorithm for the following central problem in probabilistic verification: Compute the maximal end-component (MEC) decomposition of Markov decision processes (MDPs). This problem generalizes the SCC decomposition problem of graphs and closed recurrent sets of Markov chains. The model of symbolic algorithms is widely used in formal verification and model-checking, where access to the input model is restricted to only symbolic operations (e.g., basic set operations and computation of one-step neighborhood). For an input MDP with  n  vertices and  m  edges, the classical symbolic algorithm from the 1990s for the MEC decomposition requires  O(n2)  symbolic operations and  O(1)  symbolic space. The only other symbolic algorithm for the MEC decomposition requires  O(nm−−√)  symbolic operations and  O(m−−√)  symbolic space. A main open question is whether the worst-case  O(n2)  bound for symbolic operations can be beaten. We present a symbolic algorithm that requires  O˜(n1.5)  symbolic operations and  O˜(n−−√)  symbolic space. Moreover, the parametrization of our algorithm provides a trade-off between symbolic operations and symbolic space: for all  0<ϵ≤1/2  the symbolic algorithm requires  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space ( O˜  hides poly-logarithmic factors). Using our techniques we present faster algorithms for computing the almost-sure winning regions of  ω -regular objectives for MDPs. We consider the canonical parity objectives for  ω -regular objectives, and for parity objectives with  d -priorities we present an algorithm that computes the almost-sure winning region with  O˜(n2−ϵ)  symbolic operations and  O˜(nϵ)  symbolic space, for all  0<ϵ≤1/2 ."}],"month":"07","doi":"10.1109/LICS52264.2021.9470739","isi":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.07466"}],"status":"public","project":[{"name":"Game Theory","grant_number":"S11407","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"citation":{"ama":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. Symbolic time and space tradeoffs for probabilistic verification. In: <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>. IEEE; 2021:1-13. doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>","chicago":"Chatterjee, Krishnendu, Wolfgang Dvorak, Monika Henzinger, and Alexander Svozil. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, 1–13. IEEE, 2021. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>.","ista":"Chatterjee K, Dvorak W, Henzinger M, Svozil A. 2021. Symbolic time and space tradeoffs for probabilistic verification. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS: Logic in Computer Science, 1–13.","ieee":"K. Chatterjee, W. Dvorak, M. Henzinger, and A. Svozil, “Symbolic time and space tradeoffs for probabilistic verification,” in <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, Rome, Italy, 2021, pp. 1–13.","short":"K. Chatterjee, W. Dvorak, M. Henzinger, A. Svozil, in:, Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2021, pp. 1–13.","mla":"Chatterjee, Krishnendu, et al. “Symbolic Time and Space Tradeoffs for Probabilistic Verification.” <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i>, IEEE, 2021, pp. 1–13, doi:<a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">10.1109/LICS52264.2021.9470739</a>.","apa":"Chatterjee, K., Dvorak, W., Henzinger, M., &#38; Svozil, A. (2021). Symbolic time and space tradeoffs for probabilistic verification. In <i>Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science</i> (pp. 1–13). Rome, Italy: IEEE. <a href=\"https://doi.org/10.1109/LICS52264.2021.9470739\">https://doi.org/10.1109/LICS52264.2021.9470739</a>"},"date_published":"2021-07-07T00:00:00Z"},{"license":"https://creativecommons.org/publicdomain/zero/1.0/","article_processing_charge":"No","has_accepted_license":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"ec_funded":1,"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","fulldoi":"https://doi.org/10.15479/AT:ISTA:28","date_updated":"2025-09-23T08:23:15Z","keyword":["Markov Decision Process","Decision Tree","Probabilistic Verification","Counterexample Explanation"],"month":"08","related_material":{"record":[{"id":"1603","status":"public","relation":"popular_science"}]},"abstract":[{"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.","lang":"eng"}],"oa_version":"Published Version","publist_id":"5564","type":"research_data","tmp":{"image":"/images/cc_0.png","short":"CC0 (1.0)","legal_code_url":"https://creativecommons.org/publicdomain/zero/1.0/legalcode","name":"Creative Commons Public Domain Dedication (CC0 1.0)"},"date_published":"2015-08-13T00:00:00Z","ddc":["004"],"citation":{"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>.","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>.","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>","short":"A. Fellner, (2015).","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.","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>","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>."},"project":[{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"status":"public","doi":"10.15479/AT:ISTA:28","year":"2015","contributor":[{"first_name":"Jan","last_name":"Kretinsky","id":"44CEF464-F248-11E8-B48F-1D18A9856A87"}],"datarep_id":"28","oa":1,"day":"13","publisher":"Institute of Science and Technology Austria","file":[{"checksum":"b8bcb43c0893023cda66c1b69c16ac62","relation":"main_file","creator":"system","access_level":"open_access","file_id":"5597","file_size":49557109,"date_updated":"2020-07-14T12:47:00Z","file_name":"IST-2015-28-v1+2_Fellner_DataRep.zip","date_created":"2018-12-12T13:02:31Z","content_type":"application/zip"}],"title":"Experimental part of CAV 2015 publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes","author":[{"full_name":"Fellner, Andreas","last_name":"Fellner","id":"42BABFB4-F248-11E8-B48F-1D18A9856A87","first_name":"Andreas"}],"file_date_updated":"2020-07-14T12:47:00Z","date_created":"2018-12-12T12:31:29Z","_id":"5549"}]