h1

001002228 001__ 1002228
001002228 005__ 20250321182241.0
001002228 0247_ $$2HBZ$$aHT030937329
001002228 0247_ $$2Laufende Nummer$$a44067
001002228 0247_ $$2datacite_doi$$a10.18154/RWTH-2025-00411
001002228 037__ $$aRWTH-2025-00411
001002228 041__ $$aEnglish
001002228 082__ $$a004
001002228 1001_ $$0P:(DE-82)IDM04246$$aSalmani Barzoki, Bahare$$b0$$urwth
001002228 245__ $$aProbabilistic model checking and parameter tuning for Bayesian networks$$cvorgelegt von Bahare Salmani Barzoki, M. Sc.$$honline
001002228 260__ $$aAachen$$bRWTH Aachen University$$c2024
001002228 260__ $$c2025
001002228 300__ $$a1 Online-Ressource : Illustrationen
001002228 3367_ $$02$$2EndNote$$aThesis
001002228 3367_ $$0PUB:(DE-HGF)11$$2PUB:(DE-HGF)$$aDissertation / PhD Thesis$$bphd$$mphd
001002228 3367_ $$2BibTeX$$aPHDTHESIS
001002228 3367_ $$2DRIVER$$adoctoralThesis
001002228 3367_ $$2DataCite$$aOutput Types/Dissertation
001002228 3367_ $$2ORCID$$aDISSERTATION
001002228 502__ $$aDissertation, RWTH Aachen University, 2024$$bDissertation$$cRWTH Aachen University$$d2024$$gFak01$$o2024-10-11
001002228 500__ $$aVeröffentlicht auf dem Publikationsserver der RWTH Aachen University 2025
001002228 5203_ $$aWahrscheinlichkeitsbasierte Argumentation ist zentral für den Umgang mit Unsicherheiten und das Treffen von Entscheidungen auf der Grundlage unvollständiger Beobachtungen. Bayessche Netzwerke (BNs) sind beliebte probabilistische grafische Modelle in der probabilistischen Entscheidungsfindung und Künstlichen Intelligenz (KI) und finden breite Anwendung in Bereichen wie maschinellem Lernen, Medizin, genregulatorischen Netzwerken und Finanzen. Die zentrale Aufgabe in Bayesschen Netzwerken ist die probabilistische Inferenz, die auf die Berechnung bedingter Wahrscheinlichkeiten hinausläuft. Während es eine Reihe effizienter Algorithmen für die Inferenz in BNs mit bestimmten Topologien, wie solchen mit begrenzter Baumweite, gibt, bleibt probabilistische Inferenz im Allgemeinen rechnerisch schwierig; die theoretische Komplexität ist PP-complete. Probabilistisches Model Checking (PMC) ist ein Bereich der formalen Verifikation, der sich auf die Analyse stochastischer Systeme in Bezug auf eine Menge formal definierter Eigenschaften konzentriert. Die stochastischen Systeme werden typischerweise als Markov-Modelle modelliert, und die Eigenschaften als probabilistische Erweiterungen von LTL oder CTL. Die Eigenschaften werden meist auf eine zentrale Aufgabe reduziert, nämlich die Berechnung von Erreichbarkeitswahrscheinlichkeiten. Neuere Fortschritte in diesem Bereich befassen sich mit parametrischen Erweiterungen von Markov-Modellen, bei denen ein Teil der Wahrscheinlichkeiten im Modell unbekannt ist. In dieser Dissertation stellen wir einen neuartigen Ansatz vor, der auf probabilistischem Model Checking basiert, um Inferenz und Parametertuning in Bayesschen Netzwerken durchzuführen. Die Dissertation gliedert sich in zwei Hauptszenarien: nicht-parametrisch und parametrisch. Im nicht-parametrischen Szenario konzentrieren wir uns auf klassische Bayessche Netzwerke, bei denen das Modell vollständig spezifiziert ist. Wir behandeln die bedingte Inferenz in klassischen BNs: wir präsentieren Abbildungen von Bayesschen Netzwerken in diskrete Markov-Ketten und reduzieren mathematisch die Durchführung der bedingten Inferenz in einem BN auf die Berechnung von Erreichbarkeitswahrscheinlichkeiten in Markov-Ketten. Dies ermöglicht den Einsatz modernster Algorithmen aus PMC sowie Optimierungstechniken wie Bisimulationsminimierung für die Bayessche Inferenz. Wir nutzen explizite und symbolische Methoden und evaluieren unser Framework empirisch im Vergleich zur modernen gewichteten Modellzählung. Im parametrischen Szenario betrachten wir parametrische Bayessche Netzwerke (pBNs), bei denen ein Teil der lokalen Wahrscheinlichkeitsverteilungen als Polynome über Variablen und nicht als konkrete Wahrscheinlichkeiten modelliert ist. Wir behandeln spezifisch Sensitivitätsanalysen und Parameter-Tuning-Probleme (Verhältnis-/Differenzprobleme) aus der BN-Literatur sowie das Problem der Parameterraumaufteilung aus der PMC-Literatur. Wir schlagen einen Algorithmus für das Problem des minimalen Distanz-Parameter-Tunings vor, dessen Ziel es ist, eine Instanziierung der unbekannten Parameter zu finden, die die interessierende Einschränkung erfüllt und gleichzeitig minimal von der ursprünglichen Instanziierung im gegebenen Referenzmodell abweicht. Unsere detaillierten experimentellen Bewertungen zeigen, dass unsere Parameter-Synthese-Techniken Parameter-Synthese für Bayessche Netzwerke (mit Hunderten unbekannter Parameter) behandeln können, was über die Fähigkeiten bestehender Techniken für Bayessche Netzwerke mit unbekannten Wahrscheinlichkeiten hinausgeht. Wir überwinden die strengen Einschränkungen in der Literatur bezüglich der Anzahl unbekannter Parameter, der globalen Abhängigkeiten zwischen den Parametern und der Form der erhaltenen Lösungen.$$lger
001002228 520__ $$aProbabilistic reasoning is a key to handling uncertainties and making decisions based on partial observations. Bayesian networks (BNs) are popular probabilistic graphical models in probabilistic decision-making and AI and have a wide range of applications, including machine learning, medicine, gene regulatory networks, and finance. The pivotal task in Bayesian networks is probabilistic inference that amounts to computing conditional probabilities. While there is a range of efficient algorithms for inference in BNs with certain topologies, such as those with bounded tree-width, probabilistic inference remains computationally hard in general; the theoretical complexity is PP-complete. Probabilistic model checking (PMC) is a field in formal verification that focuses on analyzing stochastic systems with respect to a set of formally defined properties. The stochastic systems are typically modelled as Markov models, and the properties as probabilistic extensions of LTL or CTL. The properties are mostly reduced to a pivotal task, computing reachability probabilities. Recent advancements in the field consider parametric extensions of Markov models, where a subset of the probabilities in the model is unknown. In this dissertation, we introduce a novel approach based on probabilistic model checking for inference and parameter tuning in Bayesian networks. The dissertation is categorized into two main settings: non-parameteric and parameteric. In the non-parameteric setting, we focus on classical Bayesian networks, where the model is fully specified. We address conditional inference on classical BNs: we present mappings from Bayesian networks into discrete-time Markov chains and mathematically reduce performing conditional inference in the BN to computing reachability probabilities in MCs. This enables applying state-of-the-art algorithms from PMC and optimization techniques such as bisimulation minimization for Bayesian inference. We exploit explicit and symbolic methods and empirically evaluate our framework against the state-of-the-art weighted model counting. In the parametric setting, we consider parametric Bayesian networks (pBNs), where a subset of local probability distributions are based polynomials over variables rather than concrete probabilities. We specifically address sensitivity analysis and ratio/difference parameter tuning problems from the BN literature, and the parameter space partitioning problem from PMC literature. We propose an algorithm for the problem of minimal distance parameter tuning, where the objective is to find an instantiation for the unknown parameters that satisfy the constraint of interest while minimally deviating from the original instantiation in the given reference model. Our detailed experimental evaluations indicate that our parameter synthesis techniques can treat parameter synthesis for Bayesian networks (with hundreds of unknown parameters), which goes beyond the capabilities of existing techniques for Bayesian networks with unknown probabilities. We lift the severe restrictions in the literature on the number of unknown parameters, the global dependencies between the parameters, and the form of obtained solutions.$$leng
001002228 536__ $$0G:(EU-Grant)787914$$aFRAPPANT - Formal Reasoning About Probabilistic Programs: Breaking New Ground for Automation (787914)$$c787914$$fERC-2017-ADG$$x0
001002228 588__ $$aDataset connected to Lobid/HBZ
001002228 591__ $$aGermany
001002228 653_7 $$aBayesian networks
001002228 653_7 $$aMarkov models
001002228 653_7 $$aformal verification
001002228 653_7 $$aparameter tuning
001002228 653_7 $$aprobabilistic graphical models
001002228 653_7 $$aprobabilistic model checking
001002228 653_7 $$asensitivity analysis
001002228 7001_ $$0P:(DE-82)IDM00048$$aKatoen, Joost-Pieter$$b1$$eThesis advisor$$urwth
001002228 7001_ $$ade Raedt, Luc$$b2$$eThesis advisor
001002228 8564_ $$uhttps://publications.rwth-aachen.de/record/1002228/files/1002228.pdf$$yOpenAccess
001002228 8564_ $$uhttps://publications.rwth-aachen.de/record/1002228/files/1002228_source.zip$$yRestricted
001002228 909CO $$ooai:publications.rwth-aachen.de:1002228$$pdnbdelivery$$pec_fundedresources$$pVDB$$pdriver$$popen_access$$popenaire
001002228 915__ $$0StatID:(DE-HGF)0510$$2StatID$$aOpenAccess
001002228 9141_ $$y2024
001002228 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM04246$$aRWTH Aachen$$b0$$kRWTH
001002228 9101_ $$0I:(DE-588b)36225-6$$6P:(DE-82)IDM00048$$aRWTH Aachen$$b1$$kRWTH
001002228 9201_ $$0I:(DE-82)121310_20140620$$k121310$$lLehrstuhl für Softwaremodellierung und Verifikation (Informatik 2)$$x0
001002228 9201_ $$0I:(DE-82)120000_20140620$$k120000$$lFachgruppe Informatik$$x1
001002228 961__ $$c2025-03-20T11:25:39.241918$$x2025-01-14T13:58:49.602451$$z2025-03-20T11:25:39.241918
001002228 9801_ $$aFullTexts
001002228 980__ $$aI:(DE-82)120000_20140620
001002228 980__ $$aI:(DE-82)121310_20140620
001002228 980__ $$aUNRESTRICTED
001002228 980__ $$aVDB
001002228 980__ $$aphd