Runtime Monitoring of Static Fairness Properties

Runtime Monitoring of Static Fairness Properties | Research Square window.SnipcartSettings = { analytics: { enabled: false } }; (function() { var accessVector = localStorage.getItem('access_vector') || ''; window.dataLayer = window.dataLayer || []; if (accessVector) { window.dataLayer.push({ user: { profile: { profileInfo: { snid: accessVector } } } }); } })(); (function(w,d,s,l,i){w[l]=w[l]||[];w[l].push({'gtm.start':new Date().getTime(),event:'gtm.js'});var f=d.getElementsByTagName(s)[0],j=d.createElement(s),dl=l!='dataLayer'?'&l='+l:'';j.async=true;j.src='https://www.googletagmanager.com/gtm.js?id='+i+dl;f.parentNode.insertBefore(j,f);})(window,document,'script','dataLayer','GTM-K279D39R'); Browse Preprints In Review Journals COVID-19 Preprints AJE Video Bytes Research Tools Research Promotion AJE Professional Editing AJE Rubriq About Preprint Platform In Review Editorial Policies Our Team Advisory Board Help Center Sign In Submit a Preprint Cite Share Download PDF Research Article Runtime Monitoring of Static Fairness Properties Thomas A. Henzinger, Mahyar Karimi, Konstantin Kueffner, Kaushik Mallik This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-7074584/v1 This work is licensed under a CC BY 4.0 License Status: Under Review Version 1 posted 7 You are reading this latest preprint version Abstract Machine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present a general framework of runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure, with or without full observation of the state space. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. We present two categories of monitoring algorithms, namely ones with a uniform error bound across all time points, and ones with weaker non-uniform, pointwise error bounds at different time points. Our monitoring algorithms use statistical tools that are adapted to suit the dynamic requirements of monitoring and the special needs of the fairness specifications. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. In these experiments, our monitors took less than a millisecond to update their verdicts after each observation. Algorithmic Fairness Formal Verification Runtime Monitoring Statistics Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Under Review Version 1 posted Reviewers agreed at journal 09 Feb, 2026 Reviews received at journal 01 Feb, 2026 Reviewers agreed at journal 25 Nov, 2025 Reviewers invited by journal 25 Nov, 2025 Editor assigned by journal 13 Aug, 2025 Submission checks completed at journal 10 Jul, 2025 First submitted to journal 08 Jul, 2025 You are reading this latest preprint version Research Square lets you share your work early, gain feedback from the community, and start making changes to your manuscript prior to peer review in a journal. As a division of Research Square Company, we’re committed to making research communication faster, fairer, and more useful. We do this by developing innovative software and high quality services for the global research community. Our growing team is made up of researchers and industry professionals working together to solve the most critical problems facing scientific publishing. Also discoverable on Platform About Our Team In Review Editorial Policies Advisory Board Help Center Resources Author Services Accessibility API Access RSS feed Manage Cookie Preferences © Research Square 2026 | ISSN 2693-5015 (online) Privacy Policy Terms of Service Do Not Sell My Personal Information {"props":{"pageProps":{"initialData":{"identity":"rs-7074584","acceptedTermsAndConditions":true,"allowDirectSubmit":false,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":550640929,"identity":"72d63dd6-c491-4886-860e-7e6e4540154c","order_by":0,"name":"Thomas A. Henzinger","email":"","orcid":"","institution":"Institute of Science and Technology Austria","correspondingAuthor":false,"prefix":"","firstName":"Thomas","middleName":"A.","lastName":"Henzinger","suffix":""},{"id":550640930,"identity":"0fe53643-d008-408c-8fa9-36f3fad4c547","order_by":1,"name":"Mahyar Karimi","email":"","orcid":"","institution":"Institute of Science and Technology Austria","correspondingAuthor":false,"prefix":"","firstName":"Mahyar","middleName":"","lastName":"Karimi","suffix":""},{"id":550640931,"identity":"69fb3535-ddcb-45a3-8076-7dd87c65f44f","order_by":2,"name":"Konstantin Kueffner","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAABJUlEQVRIie2QvWrDMBCAzwjUxanXMy7OKygY3PZtbAyeMnT0EIKhoCxJ5w59GBWBvaidNRSayVMHl0DJYEIFSSDF7s/YQd+gu5P4uNMBWCz/EDwmFICYEHrmcNbJb4ow8aBEfmkSlgDbv4sfFDhRqKm+V/zFSm7a2cv8PChJ5BYML89WTbHuOvAWwtm0fSVwn3MUVYP0QpDMVQyvl3WsU84AVUJwoEuI0xgElUgxIXLEuznTOdVpaQbTZt5hJWrF7qjsGLLXht4kHYOxBrIdUAKcMnzkeyUblUbRlEJCGTBt9jD0/aWK8elO+hzT28lDZRSVE0x55E5Uyq/UwJLrZdQWH9Ib32cS32ZGqSvnfduFYVhLqYu+coJTfind3o3FYrFY/swnGxFjI4sj3eQAAAAASUVORK5CYII=","orcid":"","institution":"Institute of Science and Technology Austria","correspondingAuthor":true,"prefix":"","firstName":"Konstantin","middleName":"","lastName":"Kueffner","suffix":""},{"id":550640932,"identity":"d5bd6d37-05b3-40ea-8549-534b6151d2b9","order_by":3,"name":"Kaushik Mallik","email":"","orcid":"","institution":"IMDEA Software","correspondingAuthor":false,"prefix":"","firstName":"Kaushik","middleName":"","lastName":"Mallik","suffix":""}],"badges":[],"createdAt":"2025-07-08 11:54:27","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-7074584/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-7074584/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":97141672,"identity":"742118f7-5fb7-4702-b470-63efae5d59b4","added_by":"auto","created_at":"2025-12-01 10:06:53","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":708510,"visible":true,"origin":"","legend":"","description":"","filename":"FMSD25.pdf","url":"https://assets-eu.researchsquare.com/files/rs-7074584/v1_covered_6d90f074-d6c5-4f65-91dc-156f9ba23fe1.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Runtime Monitoring of Static Fairness Properties","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":false,"highlight":"","institution":"","isAcceptedByJournal":false,"isAuthorSuppliedPdf":true,"isDeskRejected":"","isHiddenFromSearch":false,"isInQc":false,"isInWorkflow":false,"isPdf":true,"isPdfUpToDate":true,"isWithdrawnOrRetracted":false,"journal":{"display":true,"email":"[email protected]","identity":"formal-methods-in-system-design","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"form","sideBox":"Learn more about [Formal Methods in System Design](https://www.springer.com/journal/10703)","snPcode":"10703","submissionUrl":"https://submission.springernature.com/new-submission/10703/3","title":"Formal Methods in System Design","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"stoa","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false},"keywords":"Algorithmic Fairness, Formal Verification, Runtime Monitoring, Statistics","lastPublishedDoi":"10.21203/rs.3.rs-7074584/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-7074584/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"\u003cp\u003eMachine-learned systems are in widespread use for making decisions about humans, and it is important that they are fair, i.e., not biased against individuals based on sensitive attributes. We present a general framework of runtime verification of algorithmic fairness for systems whose models are unknown, but are assumed to have a Markov chain structure, with or without full observation of the state space. We introduce a specification language that can model many common algorithmic fairness properties, such as demographic parity, equal opportunity, and social burden. We build monitors that observe a long sequence of events as generated by a given system, and output, after each observation, a quantitative estimate of how fair or biased the system was on that run until that point in time. The estimate is proven to be correct modulo a variable error bound and a given confidence level, where the error bound gets tighter as the observed sequence gets longer. We present two categories of monitoring algorithms, namely ones with a uniform error bound across all time points, and ones with weaker non-uniform, pointwise error bounds at different time points.\u0026nbsp;Our monitoring algorithms use statistical tools that are adapted to suit the dynamic requirements of monitoring and the special needs of the fairness specifications. Using a prototype implementation, we show how we can monitor if a bank is fair in giving loans to applicants from different social backgrounds, and if a college is fair in admitting students while maintaining a reasonable financial burden on the society. In these experiments, our monitors took less than a millisecond to update their verdicts after each observation.\u003c/p\u003e","manuscriptTitle":"Runtime Monitoring of Static Fairness Properties","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2025-12-01 08:33:00","doi":"10.21203/rs.3.rs-7074584/v1","editorialEvents":[{"type":"communityComments","content":0},{"type":"reviewerAgreed","content":"34757140523165426765039996260962831813","date":"2026-02-09T16:56:31+00:00","index":"hide","fulltext":""},{"type":"editorInvitedReview","content":"","date":"2026-02-01T20:30:00+00:00","index":"hide","fulltext":""},{"type":"reviewerAgreed","content":"837588804554168427483097293178319939","date":"2025-11-25T14:18:10+00:00","index":"hide","fulltext":""},{"type":"reviewersInvited","content":"","date":"2025-11-25T13:59:56+00:00","index":"","fulltext":""},{"type":"editorAssigned","content":"","date":"2025-08-13T13:02:30+00:00","index":"","fulltext":""},{"type":"checksComplete","content":"","date":"2025-07-10T09:06:40+00:00","index":"","fulltext":""},{"type":"submitted","content":"Formal Methods in System Design","date":"2025-07-08T11:43:19+00:00","index":"","fulltext":""}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"formal-methods-in-system-design","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":false,"externalIdentity":"form","sideBox":"Learn more about [Formal Methods in System Design](https://www.springer.com/journal/10703)","snPcode":"10703","submissionUrl":"https://submission.springernature.com/new-submission/10703/3","title":"Formal Methods in System Design","twitterHandle":"","acdcEnabled":true,"dfaEnabled":true,"editorialSystem":"stoa","reportingPortfolio":"Springer Hybrid","inReviewEnabled":true,"inReviewRevisionsEnabled":false}}],"origin":"","ownerIdentity":"fffa7508-a31c-49e5-9490-8e6ae4c34f5e","owner":[],"postedDate":"December 1st, 2025","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"under-review","subjectAreas":[],"tags":[],"updatedAt":"2025-12-01T08:33:00+00:00","versionOfRecord":[],"versionCreatedAt":"2025-12-01 08:33:00","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-7074584","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-7074584","identity":"rs-7074584","version":["v1"]},"buildId":"8U1c8b4HqxoKbykW_rLl7","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}