Formal specification and verification of rule-basedartificial intelligence systems using Event-B

Formal specification and verification of rule-basedartificial intelligence systems using Event-B | 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 Formal specification and verification of rule-basedartificial intelligence systems using Event-B Thanh Binh Trinh, Ninh Thuan Truong This is a preprint; it has not been peer reviewed by a journal. https://doi.org/ 10.21203/rs.3.rs-7313564/v1 This work is licensed under a CC BY 4.0 License Status: Posted Version 1 posted You are reading this latest preprint version Abstract Rule-based artificial intelligence (RB-AI) systems offer a high degree of interpretability and control, making them particularly suitable for safety-critical domains such as healthcare, transportation, and industrial automation. However, ensuring their correctness is challenging, as rule interactions may cause logical conflicts, redundancies, and livelocks—issues difficult to detect through conventional testing, especially in dynamic environments.This article presents a formal approach for the specification and verification of RB-AI systems using Event-B, a state-based formal method grounded in set theory and first-order logic. In this approach, rule activation, condition monitoring, and action execution are specified as part of a formal Event-B model, where critical properties—such as safety, liveness, conflict freedom, redundancy elimination, and livelock prevention—are encoded as invariants and theorems. These properties are automatically verified using the Rodin platform, which generates and discharges proof obligations to ensure rule execution is both sound and traceable.A case study on SmartAir, an AI-driven fan control system, demonstrates how the method detects rule conflicts, eliminates redundant behavior, and prevents livelocks. The results show that the approach provides a solid foundation for building RB-AI systems with formal assurance and applicability to real-world contexts where verifiability is essential. Rule-based AI systems reactive systems formal verification Event-B Rodin platform Full Text Additional Declarations No competing interests reported. Cite Share Download PDF Status: Posted Version 1 posted 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-7313564","acceptedTermsAndConditions":true,"allowDirectSubmit":true,"archivedVersions":[],"articleType":"Research Article","associatedPublications":[],"authors":[{"id":510097015,"identity":"2c4a5e04-71d0-4500-85b9-0a7e66a1ed01","order_by":0,"name":"Thanh Binh Trinh","email":"data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAZAAAAAyAQMAAABI0h/eAAAABlBMVEX///8AAABVwtN+AAAACXBIWXMAAA7EAAAOxAGVKw4bAAABR0lEQVRIie2Qv0vDQBTHXwkky1XXK7H2X7hQSChV+69cCDRLooOLoOBBIJPS1aF/hJt2MnIQl/sDbhDJlEkhk9RB8ZJWiK0/VsF8lvty733ePQ6goeEPQjTQyxMBrkKyrQIATRZldWhfK7RUtErp/67AQoEPxWV42btkTXGMdpq15g9bjjlJs5fre//KjNIsE3s9wOFtAkdDNSRMasog2vAJ0EM0mHLDOhd5OJumPqHSsxjeV/sJ3y1DfTGObAyUIiI9HbdjHl7KwMa00Fo3MiBJK+YuQ4J8p3ReY+4TefCslNMRw6Xy9rNiqlcokYGOqVSdlcJUMM7qyiBSCh1Xim12Y27NLsbqRtx5DD2ShKZ+P/6sOJvCxsUOHRHp5p2nmPcc7OWdeXq8y4ygXxQnw+5EQ3Wlov4fQNZK+mr/KmsDGxoaGv49704BfMzfEkPLAAAAAElFTkSuQmCC","orcid":"","institution":"Phenikaa University","correspondingAuthor":true,"prefix":"","firstName":"Thanh","middleName":"Binh","lastName":"Trinh","suffix":""},{"id":510097016,"identity":"be316fab-6eb5-4ff6-8b81-689bdb30776d","order_by":1,"name":"Ninh Thuan Truong","email":"","orcid":"","institution":"VNU University of Engineering and Technology","correspondingAuthor":false,"prefix":"","firstName":"Ninh","middleName":"Thuan","lastName":"Truong","suffix":""}],"badges":[],"createdAt":"2025-08-07 01:08:09","currentVersionCode":1,"declarations":"","doi":"10.21203/rs.3.rs-7313564/v1","doiUrl":"https://doi.org/10.21203/rs.3.rs-7313564/v1","draftVersion":[],"editorialEvents":[],"editorialNote":"","failedWorkflow":false,"files":[{"id":106458044,"identity":"b724d79c-49e8-407e-a2df-f4b58149578a","added_by":"auto","created_at":"2026-04-08 18:40:24","extension":"pdf","order_by":1,"title":"","display":"","copyAsset":false,"role":"manuscript-pdf","size":589711,"visible":true,"origin":"","legend":"","description":"","filename":"ASE.pdf","url":"https://assets-eu.researchsquare.com/files/rs-7313564/v1_covered_00298f22-5584-406a-a603-a3458e20df00.pdf"}],"financialInterests":"No competing interests reported.","formattedTitle":"Formal specification and verification of rule-basedartificial intelligence systems using Event-B","fulltext":[],"fulltextSource":"","fullText":"","funders":[],"hasAdminPriorityOnWorkflow":false,"hasManuscriptDocX":false,"hasOptedInToPreprint":true,"hasPassedJournalQc":"","hasAnyPriority":false,"hideJournal":true,"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":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true},"keywords":"Rule-based AI systems, reactive systems, formal verification, Event-B, Rodin platform","lastPublishedDoi":"10.21203/rs.3.rs-7313564/v1","lastPublishedDoiUrl":"https://doi.org/10.21203/rs.3.rs-7313564/v1","license":{"name":"CC BY 4.0","url":"https://creativecommons.org/licenses/by/4.0/"},"manuscriptAbstract":"Rule-based artificial intelligence (RB-AI) systems offer a high degree of interpretability and control, making them particularly suitable for safety-critical domains such as healthcare, transportation, and industrial automation. However, ensuring their correctness is challenging, as rule interactions may cause logical conflicts, redundancies, and livelocks—issues difficult to detect through conventional testing, especially in dynamic environments.This article presents a formal approach for the specification and verification of RB-AI systems using Event-B, a state-based formal method grounded in set theory and first-order logic. In this approach, rule activation, condition monitoring, and action execution are specified as part of a formal Event-B model, where critical properties—such as safety, liveness, conflict freedom, redundancy elimination, and livelock prevention—are encoded as invariants and theorems. These properties are automatically verified using the Rodin platform, which generates and discharges proof obligations to ensure rule execution is both sound and traceable.A case study on SmartAir, an AI-driven fan control system, demonstrates how the method detects rule conflicts, eliminates redundant behavior, and prevents livelocks. The results show that the approach provides a solid foundation for building RB-AI systems with formal assurance and applicability to real-world contexts where verifiability is essential.","manuscriptTitle":"Formal specification and verification of rule-basedartificial intelligence systems using Event-B","msid":"","msnumber":"","nonDraftVersions":[{"code":1,"date":"2025-09-12 06:46:18","doi":"10.21203/rs.3.rs-7313564/v1","editorialEvents":[{"type":"communityComments","content":0}],"status":"published","journal":{"display":true,"email":"[email protected]","identity":"researchsquare","isNatureJournal":false,"hasQc":true,"allowDirectSubmit":true,"externalIdentity":"","sideBox":"","snPcode":"","submissionUrl":"/submission","title":"Research Square","twitterHandle":"researchsquare","acdcEnabled":true,"dfaEnabled":false,"editorialSystem":"","reportingPortfolio":"","inReviewEnabled":false,"inReviewRevisionsEnabled":true}}],"origin":"","ownerIdentity":"8c56f5ea-edd1-4192-a713-130d9bf7cd54","owner":[],"postedDate":"September 12th, 2025","published":true,"recentEditorialEvents":[],"rejectedJournal":[],"revision":"","amendment":"","status":"posted","subjectAreas":[],"tags":[],"updatedAt":"2026-04-08T18:40:10+00:00","versionOfRecord":[],"versionCreatedAt":"2025-09-12 06:46:18","video":"","vorDoi":"","vorDoiUrl":"","workflowStages":[]},"version":"v1","identity":"rs-7313564","journalConfig":"researchsquare"},"__N_SSP":true},"page":"/article/[identity]/[[...version]]","query":{"redirect":"/article/rs-7313564","identity":"rs-7313564","version":["v1"]},"buildId":"8U1c8b4HqxoKbykW_rLl7","isFallback":false,"isExperimentalCompile":false,"dynamicIds":[84888],"gssp":true,"scriptLoader":[]}