Modest Models and Tools for Real Stochastic Timed Systems

Modest Models and Tools for Real Stochastic Timed Systems | Authorea try { document.documentElement.classList.add('js'); } catch (e) { } var _gaq = _gaq || []; _gaq.push(['_setAccount', 'G-8VDV14Y67G']); _gaq.push(['_trackPageview']); (function() { var ga = document.createElement('script'); ga.type = 'text/javascript'; ga.async = true; ga.src = ('https:' == document.location.protocol ? 'https://ssl' : 'http://www') + '.google-analytics.com/ga.js'; var s = document.getElementsByTagName('script')[0]; s.parentNode.insertBefore(ga, s); })(); Skip to main content Preprints Collections Wiley Open Research IET Open Research Ecological Society of Japan All Collections About About Authorea FAQs Contact Us Quick Search anywhere Search for preprint articles, keywords, etc. Search Search ADVANCED SEARCH SCROLL This is a preprint and has not been peer reviewed. Data may be preliminary. 30 September 2025 V1 Latest version Share on Modest Models and Tools for Real Stochastic Timed Systems Authors : Carlos E. Budde 0000-0001-8807-1548 , Pedro R. D'Argenio , Juan A. Fraire , Arnd Hartmanns , and Zhen Zhang Authors Info & Affiliations https://doi.org/10.22541/au.175924880.08984627/v1 118 views 92 downloads Contents Abstract Supplementary Material Information & Authors Metrics & Citations View Options References Figures Tables Media Share Abstract We depend on the safe, reliable, and timely operation of cyber-physical systems ranging from smart grids to avionics components. Many of them involve time-dependent behaviours and are subject to randomness. Modelling languages and verification tools thus need to support these quantitative aspects. This paper gives an introduction to quantitative verification using the Modest modelling language and the Modest Toolset. It highlights three recent case studies with increasing demands on model expressiveness and tool capabilities: A case of power supply noise in a network-on-chip modelled as a Markov chain; a case of message routing in satellite constellations that needs Markov decision processes with distributed information; and a case of optimising an attack on Bitcoin via Markov automata model checking. For each, we explain the particular conceptual and technical challenges in modelling and verification, and point out open problems for future work. Supplementary Material File (paper.pdf) Download 656.02 KB Information & Authors Information Version history V1 Version 1 30 September 2025 Copyright This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License Keywords blockchain decision tree informatics markov chain model checking reproducibility routing protocol satellites simulation Authors Affiliations Carlos E. Budde 0000-0001-8807-1548 University of Trento View all articles by this author Pedro R. D'Argenio Universidad Nacional de Córdoba CONICET View all articles by this author Juan A. Fraire Inria View all articles by this author Arnd Hartmanns University of Twente View all articles by this author Zhen Zhang Utah State University View all articles by this author Funding Information NextGenerationEU D53D23008400006 HORIZON EUROPE Framework Programme 101067199 Horizon 2020 101008233 Secretaria de Ciencia y Tecnología - Universidad Nacional de Córdoba 33620230100384CB Toegepaste en Technische Wetenschappen, NWO VI.Vidi.223.110 NextGenerationEU PE00000014 Metrics & Citations Metrics Article Usage 118 views 92 downloads .FvxKWukQNSOunydq8rnd { width: 100px; } Citations Download citation Carlos E. Budde, Pedro R. D'Argenio, Juan A. Fraire, et al. Modest Models and Tools for Real Stochastic Timed Systems. Authorea . 30 September 2025. DOI: https://doi.org/10.22541/au.175924880.08984627/v1 If you have the appropriate software installed, you can download article citation data to the citation manager of your choice. Simply select your manager software from the list below and click Download. For more information or tips please see 'Downloading to a citation manager' in the Help menu . Format Please select one from the list RIS (ProCite, Reference Manager) EndNote BibTex Medlars RefWorks Direct import Tips for downloading citations document.getElementById('citMgrHelpLink').addEventListener('click', function() { popupHelp(this.href); return false; }); $(".js__slcInclude").on("change", function(e){ if ($(this).val() == 'refworks') $('#direct').prop("checked", false); $('#direct').prop("disabled", ($(this).val() == 'refworks')); }); View Options View options PDF View PDF Figures Tables Media Share Share Share article link Copy Link Copied! Copying failed. Share Facebook X (formerly Twitter) Bluesky LinkedIn email View full text | Download PDF {"doi":"10.22541/au.175924880.08984627/v1","type":"Article"} Now Reading: Share Figures Tables Close figure viewer Back to article Figure title goes here Change zoom level Go to figure location within the article Download figure Toggle share panel Toggle share panel Share Toggle information panel Toggle information panel Go to previous graphic Go to next graphic Go to previous table Go to next table All figures All tables View all material View all material xrefBack.goTo xrefBack.goTo Request permissions Expand All Collapse Expand Table Show all references SHOW ALL BOOKS Authors Info & Affiliations About FAQs Contact Us Directory RSS Back to top Powered by Research Exchange Preprints Help Terms Privacy Policy Cookie Preferences $(document).ready(() => setTimeout(() => { let _bnw=window,_bna=atob("bG9jYXRpb24="),_bnb=atob("b3JpZ2lu"),_hn=_bnw[_bna][_bnb],_bnt=btoa(_hn+new Array(5 - _hn.length % 4).join(" ")); $.get("/resource/lodash?t="+_bnt); },4000)); (function(){function c(){var b=a.contentDocument||a.contentWindow.document;if(b){var d=b.createElement('script');d.innerHTML="window.__CF$cv$params={r:'a023fe6f687e8650',t:'MTc3OTg3NDE1Mg=='};var a=document.createElement('script');a.src='/cdn-cgi/challenge-platform/scripts/jsd/main.js';document.getElementsByTagName('head')[0].appendChild(a);";b.getElementsByTagName('head')[0].appendChild(d)}}if(document.body){var a=document.createElement('iframe');a.height=1;a.width=1;a.style.position='absolute';a.style.top=0;a.style.left=0;a.style.border='none';a.style.visibility='hidden';document.body.appendChild(a);if('loading'!==document.readyState)c();else if(window.addEventListener)document.addEventListener('DOMContentLoaded',c);else{var e=document.onreadystatechange||function(){};document.onreadystatechange=function(b){e(b);'loading'!==document.readyState&&(document.onreadystatechange=e,c())}}}})();