Tools and Algorithms for the Construction and Analysis of Systems
31st International Conference, TACAS 2025, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, Hamilton, ON, Canada, May 3–8, 2025, Proceedings, Part II
- Open Access
- 2025
- Open Access
- Buch
- Herausgegeben von
- Arie Gurfinkel
- Marijn Heule
- Buchreihe
- Lecture Notes in Computer Science
- Verlag
- Springer Nature Switzerland
Über dieses Buch
Die Open-Access-Bücher LNCS 15696, 15697 und 15698 bilden den Rahmen der 31. Internationalen Konferenz über Werkzeuge und Algorithmen für die Konstruktion und Analyse von Systemen, TACAS 2025, die im Rahmen der Internationalen Gemeinsamen Konferenzen über Theorie und Praxis von Software, ETAPS 2025, vom 3. bis 8. Mai 2025 in Hamilton, Kanada, abgehalten wurde. Die 46 präsentierten Arbeiten wurden sorgfältig geprüft und aus 148 Einreichungen ausgewählt. Zu den Verfahren gehören auch 14 Arbeiten aus dem Wettbewerb zur Softwareverifizierung, der im Rahmen von TACAS abgehalten wurde. Die Vorträge waren wie folgt in thematische Abschnitte gegliedert: Teil I: Programmanalyse, ATP und Umschreiben; Modellüberprüfung; LTL; Verifikation; Teil II: SAT- und SMT-Lösung; Beweise und Zertifikate; Synthese; Äquivalenzprüfung; Spiele; Teil III: Verifikation; Quanten- und GPU; 14. Wettbewerb zur Software-Verifikation, SV-COMP 2025.
Mit KI übersetzt
Über dieses Buch
The open access book set LNCS 15696, 15697 and 15698 constitutes the proceedings of the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2025, which was held as part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2025, during May 3-8, 2025, in Hamilton, Canada.
The 46 papers presented were carefully reviewed and selected from 148 submissions. The proceedings also include 14 papers from the Software Verification competition which was held as part of TACAS. The papers were organized in topical sections as follows:
Part I: Program analysis, ATP and rewriting; model checking; LTL; verification;
Part II: SAT and SMT solving; proofs and certificates; synthesis; equivalence checking; games;
Part III: Verification; quantum and GPU; 14th Competition on Software Verification, SV-COMP 2025.
Anzeige
Inhaltsverzeichnis
-
SAT and SMT Solving
-
Frontmatter
-
Incremental SAT-Based Enumeration of Solutions to the Yang-Baxter Equation
- Open Access
PDF-Version jetzt herunterladenDie Yang-Baxter-Gleichung (YBE) ist eine grundlegende Gleichung in der mathematischen Physik mit weitreichenden Anwendungen in verschiedenen Bereichen der reinen Mathematik, einschließlich der Repräsentationstheorie und der niederdimensionalen Topologie. Dieses Kapitel untersucht die diskrete Version des YBE und konzentriert sich auf die Konstruktion von Set-Theory-Lösungen, die aufgrund ihrer Bedeutung und Komplexität hervorgehoben wurden. Das Kapitel stellt das SAT Modulo Symmetries (SMS) Framework vor, eine Technik zur isomorphen-freien Aufzählung, und wendet es auf das YBE an. Die Autoren diskutieren, wie man die YBE in konjunktiver Normalform (CNF) kodiert und eine domänenspezifische Minimalitätsprüfung entwickelt, um nicht-isomorphe Lösungen effizient aufzuzählen. Zwei Implementierungen dieser Minimalitätsprüfung werden vorgestellt: ein Backtracking-Ansatz und ein schrittweiser SAT-basierter Ansatz. Insbesondere der inkrementelle Ansatz zeigt deutliche Beschleunigungen und ermöglicht die Aufzählung von Lösungen für Größen, die vorher unerreichbar waren. Das Kapitel enthält auch eine detaillierte experimentelle Bewertung, in der die neuen Ansätze mit bestehenden Methoden verglichen und die erzielten Leistungsverbesserungen hervorgehoben werden. Darüber hinaus wird in diesem Kapitel das Potenzial diskutiert, diese Methoden auf andere kombinatorische Strukturen auszuweiten und die Herausforderungen der Bereitstellung von Nachweisprotokollen für eine isomorphismusfreie Erzeugung zu diskutieren.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe tackle the problem of enumerating set-theoretic solutions to the Yang-Baxter equation. This equation originates from statistical and quantum mechanics, but also has applications in knot theory, cryptography, quantum computation and group theory. Non-degenerate, involutive solutions have been enumerated for sets up to size 10 using constraint programming with partial static symmetry breaking [1]; for general non-involutive solutions, a similar approach was used to enumerate solutions for sets up to size 8. In this paper, we use and extend the SAT Modulo Symmetries framework (SMS), to expand the boundaries for which solutions are known. The SMS framework relies on a minimality check; we present two solutions to this, one that stays close to the original one designed for enumerating graphs and a new incremental, SAT-based approach. With our new method, we can reproduce previously known results much faster and also report on results for sizes that have remained out of reach so far. -
Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation
- Open Access
PDF-Version jetzt herunterladenIn diesem Kapitel wird der Z3-Noodler 1.3 vorgestellt, ein hochmoderner String-Solver, der sich in der Stringabteilung von SMT-COMP '24 als überlegen erwiesen hat. Das Rahmenwerk ist so konzipiert, dass es mit einer breiten Palette von String-Beschränkungen umgehen kann, indem es mehrere Entscheidungsverfahren integriert, die jeweils auf bestimmte Arten von Beschränkungen zugeschnitten sind. Dieser Ansatz adressiert die Komplexität der String-Lösung, bei der ein einzelnes Verfahren häufig nicht ausreicht, um vielfältige Probleme der realen Welt zu lösen. Das Kapitel beschreibt die Implementierung von zwei neuen Entscheidungsverfahren: eine zur Handhabung reiner regulärer Beschränkungen unter Verwendung endlicher Automaten und eine andere zur Umwandlung von Gleichungsblockstringbeschränkungen in linear-ganzzahlige arithmetische (LIA) Beschränkungen. Darüber hinaus werden die Optimierung der Nielsen-Transformation und die Erweiterung der Möglichkeiten zur Modellerzeugung diskutiert. Die Bewertung von Z3-Noodler 1.3 anhand von Standard-SMT-LIB-Benchmarks zeigt signifikante Verbesserungen bei der Anzahl der gelösten Instanzen und der Lösungszeit im Vergleich zu anderen hochmodernen Tools. Das Kapitel bietet auch Einblicke in die Auswirkungen unterschiedlicher Entscheidungsverfahren und Modellgenerierung auf die Gesamtleistung, was es zu einer entscheidenden Lektüre für diejenigen macht, die sich für die neuesten Entwicklungen im Bereich der Stringlösungstechnologien interessieren.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractZ3-Noodler is a fork of the Z3 SMT solver replacing its string theory implementation with a portfolio of decision procedures and a selection mechanism for choosing among them based on the features of the input formula. In this paper, we give an overview of the used decision procedures, including a novel length-based procedure, and their integration into a robust solver with a good overall performance, as witnessed by Z3-Noodler winning the string division of SMT-COMP’24 by a large margin. We also extended the solver with a support for model generation, which is essential for the use of the solver in practice. -
D-Painless: A Framework for Distributed Portfolio SAT Solving
- Open Access
PDF-Version jetzt herunterladenDas Kapitel geht der entscheidenden Rolle von SAT-Formeln bei der Verschlüsselung komplexer Probleme in verschiedenen Bereichen wie Schaltkreisverifikation, Kryptographie, automatisierte Planung und Softwareverifikation nach. Es betont die Herausforderungen durch harte SAT-Instanzen und die Notwendigkeit paralleler und verteilter Rechnerumgebungen, um die Lösungszeiten zu reduzieren. Die Erweiterung des Rahmenwerks zur Aufnahme von SAT-Lösern für verteilte Klauseln ist ein wesentlicher Schwerpunkt, der die Einbeziehung diverser Klauselteilungsstrategien und Knotentopologien ermöglicht. Diese Erweiterung führt zu einem vielseitigen Framework, das die Entwicklung verteilter SAT-Solver vereinfacht und es zu einem unschätzbaren Werkzeug für Forscher macht. Das Kapitel bietet einen detaillierten Überblick über verwandte Arbeiten, einschließlich bahnbrechender Bemühungen zur Lösung verteilter SAT-Probleme und der Entwicklung von Strategien zum Austausch von Klauseln. Es präsentiert außerdem eine umfassende Bewertung der neuen Architektur, bewertet ihre Leistung anhand implementierter Sharing-Strategien und vergleicht sie mit modernen Lösungsansätzen. Das Kapitel schließt mit einer Diskussion über mögliche zukünftige Arbeiten, einschließlich der Entwicklung fehlertoleranter Algorithmen und der Optimierung bestehender Komponenten zur Steigerung der Gesamteffizienz. Die Erforschung der dezentralen Bereitstellung, der gemeinsamen Nutzung von Klauseln und der Architektur des Rahmenwerks bietet einen tiefen Einblick in die technischen Komplexitäten und innovativen Lösungen im Bereich der dezentralen SAT-Lösungen.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractIn the evolving landscape of SAT solving, leveraging parallel computation has become increasingly significant. The portfolio strategy, combined with clause sharing, has emerged as the leading approach for both local and distributed parallelization on CPUs. Frameworks such as Mallob exemplify the effectiveness of this strategy by providing a straightforward method to deploy portfolio parallel solvers across various computing environments. Similarly, the
framework specializes in local parallelization, offering diverse strategies for task sharing and parallel execution. This enables the adoption of complex hybrid local parallelization techniques, including portfolio, divide-and-conquer, and cube-and-conquer methods.
This paper presents
, a new extension of the 
framework to include the distributed portfolio strategy and clause sharing. Our enhancement aims to broaden 
’s functionality, enabling more effective and comprehensive distributed SAT solving methodologies.
-
-
Proofs and Certificates
-
Frontmatter
-
Unsatisfiability Proofs for Horn Solving
- Open Access
PDF-Version jetzt herunterladenDas Kapitel geht der kritischen Notwendigkeit von Korrektheitszeugen in beschränkten Horn-Klauseln nach, die für die Überprüfung der Korrektheit von Software und Systemen unverzichtbar sind. Es führt einen neuartigen Ansatz zur Erstellung und Instanziierung von Unbefriedigungsnachweisen ein, der eine unabhängige Validierung der Ergebnisse von CHC-Lösern ermöglicht. Der Ansatz ist generisch konzipiert und berücksichtigt verschiedene Lösungsalgorithmen, Vorverarbeitungsschritte und Proof-Formate, wodurch seine Anwendbarkeit auf verschiedene Verifikationswerkzeuge verbessert wird. Das Kapitel bietet einen umfassenden Hintergrund zu CHC-Systemen und Unbefriedigungsnachweisen und beschreibt die Erstellung grobkörniger Kornnachweise unter Verwendung des Spacer-Algorithmus und deren Rückübersetzung zur Berücksichtigung der Vorverarbeitung. Es beschreibt auch die Instanziierung dieser Grobproofs in das Alethe-Proof-Format, das von Tools wie Carcara unabhängig überprüft werden kann. Im Abschnitt Evaluierung wird eine groß angelegte Bewertung anhand von 600 Benchmarks aus dem Wettbewerb CHC-COMP 2024 präsentiert, die zeigt, dass die Erstellung und Überprüfung von Nachweisen einen minimalen Aufwand für die Lösung der Probleme mit sich bringt. Die Ergebnisse deuten darauf hin, dass der Ansatz praktisch und effizient ist, was ihn zu einem wertvollen Beitrag im Bereich der formalen Verifikation und Softwarevalidierung macht.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractMany verification tools currently rely on logic solvers as backend reasoning engines. Despite playing such a pivotal role, bugs are not uncommon in the complex codebases of these solvers. Validating their results is thus critical, with correctness witnesses often being used for this end. Output validation for constrained Horn clauses (CHC) solvers is not a well explored topic though, especially in regards to unsatisfiability results. This is a significant issue, given that CHC solvers are being increasingly employed in verification tooling. To address it, we propose an approach to validate CHC unsatisfiability results based on independently checkable proofs. Our approach is generic in regards to the solving algorithm, preprocessing steps, and exact proof format used, and works by first producing a coarse-grained proof during solving and then instantiating it into a suitable proof format by adding missing details, at which point the instantiated proof can be checked by an independent proof checker. We instrumented a state-of-the-art CHC solver to generate proofs in the Alethe format and performed a large-scale evaluation. Our results indicate that proofs can be produced with minimal overhead, can be efficiently checked, and have tractable sizes. -
Revisiting DRUP-Based Interpolants with CaDiCaL 2.0
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel befasst sich mit der Generierung von Interpolanten aus DRUP-Proofs und konzentriert sich auf ihre Anwendung bei der Überprüfung von SAT-Modellen. Es stellt Drup2Itp vor, ein Framework, das auf dem CaDiCaL 2.0 SAT-Solver aufbaut und die Tracer-API nutzt, um inkrementelle DRUP-Protokollierung im Speicher zu ermöglichen, ohne die Einbauten des Solvers zu verändern. Dieses Design ermöglicht flexible und effiziente interpolante Berechnungen, die speziell für Anwendungen zur Modellprüfung zugeschnitten sind. Das Kapitel behandelt die Implementierungsdetails von Drup2Itp, einschließlich seiner entkoppelten Architektur, spezialisierter Verfahren zur Unit Propagation und Konfliktanalyse und der Einführung eines Proof-Minimization-Algorithmus. Der Evaluierungsteil präsentiert einen gründlichen Vergleich von Drup2Itp mit bestehenden Tools unter Verwendung von Benchmarks der Hardware Model Checking Competitions (HWMCC '19 und HWMCC' 20). Die Ergebnisse zeigen, dass Drup2Itp, wenn es mit CaDiCaL integriert wird, die Leistung des Avy-Modellprüfers signifikant verbessert, mehr Fälle löst und eine bessere Laufzeitperformance im Vergleich zur Vanilla-Version erreicht. Das Kapitel untersucht auch die Auswirkungen der Beweisminimierung auf die interpolante Generierung und bietet Einblicke in das Potenzial weiterer Verbesserungen bei Interpolationstechniken und deren Anwendung bei der Modellüberprüfung.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe present our implementation of DRUP-based interpolants inCaDiCaL2.0, and evaluate performance in the bit-level model checkerAvyusing the Hardware Model Checking Competition benchmarks.CaDiCaLis a state-of-the-art, open-source SAT solver known for its efficiency and flexibility. In its latest release, version 2.0,CaDiCaLintroduces a new proof tracer API. This paper presents a tool that leverages this API to implement the DRUP-based algorithm for generating interpolants.By integrating this algorithm intoCaDiCaL, we enable its use in model-checking workflows that require interpolants. Our experimental evaluation shows that integratingCaDiCaLwith DRUP-based interpolants inAvyresults in better performance (both runtime and number of solved instances) when compared toAvywithGlucoseas the main SAT solver.Our implementation is publicly available and can be used by the formal methods community to further develop interpolation-based algorithms using the state-of-the-art SAT solverCaDiCaL. Since our implementation uses theTracerAPI, it should be maintainable and applicable to future releases ofCaDiCaL. -
Certifying Pareto-Optimality in Multi Objective Maximum Satisfiability
- Open Access
PDF-Version jetzt herunterladenDas Kapitel vertieft sich in die entscheidende Rolle automatisierten Denkens bei der Entwicklung korrekter und vertrauenswürdiger Systeme, wobei der Schwerpunkt auf Boolescher Zufriedenheit (SAT) und maximaler Zufriedenheit (MaxSAT) liegt. Es unterstreicht die Bedeutung von Nachweisprotokollierungs- und Überprüfungstechniken, um die Zuverlässigkeit der Lösergebnisse zu gewährleisten, insbesondere bei Optimierungsproblemen in der realen Welt. Der Text führt das VeriPB-Format ein, das Proof-Logging für Probleme bei der Optimierung von Einzelobjekten unterstützt und seine Anwendung auf Multiobjektiv-Lösungen von MaxSAT (MO-MaxSAT) ausweitet. Durch Nutzung von Vorbestellungen in VeriPB wird gezeigt, wie man Pareto-Optimalität in MO-MaxSAT-Algorithmen zertifiziert, um sicherzustellen, dass die berechneten Lösungen repräsentativ für den nicht dominierten Satz sind. Das Kapitel enthält detaillierte Proof-Logging-Prozeduren für verschiedene MO-MaxSAT-Algorithmen, darunter -minimal, BiOptSat und LowerBound, sowie die Kernvorverarbeitungstechnologie zur Steigerung der Leistungsfähigkeit. Experimentelle Ergebnisse zeigen, dass Proof Logging für MO-MaxSAT skalierbar gemacht werden kann, mit tolerierbaren Laufzeitkosten. Das Kapitel schließt mit der Diskussion der Implikationen dieser Erkenntnisse und potenzieller zukünftiger Arbeiten zur Ausweitung des Proof Logging auf alle Pareto-optimalen Lösungen.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractDue to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For Boolean satisfiability (SAT) solvers—and more recently SAT-based maximum satisfiability (MaxSAT) solvers—trustworthiness is obtained by integrating proof logging into solvers, making solvers capable of emitting machine-verifiable proofs to certify correctness of the reasoning steps performed. In this work, we enable for the first time proof logging based on the VeriPB proof format for multi-objective MaxSAT (MO-MaxSAT) optimization techniques. Although VeriPB does not offer direct support for multi-objective problems, we detail how preorders in VeriPB can be used to provide certificates for MO-MaxSAT algorithms computing a representative solution for each element in the non-dominated set of the search space under Pareto optimality, without extending the VeriPB format or the proof checker. By implementing VeriPB proof logging into a state-of-the-art multi-objective MaxSAT solver, we show empirically that proof logging can be made scalable for MO-MaxSAT with reasonable overhead. -
Fixed Point Certificates for Reachability and Expected Rewards in MDPs
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die kritische Notwendigkeit der Zertifizierung von Algorithmen in Markov-Entscheidungsprozessen (MDPs) und betont die Berechnung von Erreichbarkeitswahrscheinlichkeiten und erwarteten Belohnungen. Es geht auf die Schwachstellen in bestehenden MDP-Modellprüfwerkzeugen ein und hebt Fehlerquellen wie Implementierungsfehler, unsolide Algorithmen, numerische Ungenauigkeiten und Abhängigkeiten von Drittanbietern hervor. Die Autoren schlagen einen neuen Standard für zertifizierte MDP-Modellüberprüfung vor, der Festpunktzertifikate einführt, die knappe, leicht überprüfbare Nachweise der Ergebnisse liefern. Diese Zertifikate sind solide und vollständig für willkürliche endliche MDPs und gewährleisten strenge Korrektheit und Präzision. Das Kapitel formalisiert die Theorie in Isabelle / HOL und erzeugt eine formal verifizierte Zertifikatsprüfer-Implementierung. Außerdem werden praktische Implementierungen des Storm-Modellcheckers vorgestellt, die die Anwendbarkeit und Erweiterbarkeit des vorgeschlagenen Ansatzes anhand umfangreicher Experimente mit dem Quantitativen Verifikationsbenchmark Set demonstrieren. Das Kapitel schließt mit einer Diskussion über Skalierbarkeit und Effizienz der zertifizierten Pipeline, die den Weg für zukünftige Fortschritte bei der probabilistischen Modellüberprüfung ebnet.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractThe possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set.
-
-
Synthesis
-
Frontmatter
-
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
- Open Access
PDF-Version jetzt herunterladenDas Kapitel untersucht die automatisierte Synthese verteilter Protokolle, ein schwieriges Problem im Bereich der Computersysteme. Es stellt eine neue Methode vor, die das Skizzierungsparadigma nutzt, um das Syntheseproblem in ein Suchproblem zu verwandeln, wobei der Benutzer eine Protokollskizze bereitstellt, die Löcher enthält, die mit Ausdrücken aus zugehörigen Grammatiken gefüllt werden können. Die Methode folgt dem Paradigma der kontrabeispielgestützten induktiven Synthese (CEGIS), bei der ein Lernender mit einem Prüfer zusammenarbeitet, um Kandidatenprotokolle zu erstellen und zu überprüfen. Eine Schlüsselinnovation ist die Einführung der Interpretationsreduzierung, einer Technik zur Verringerung des Suchraums, die die Aufzählung redundanter Kandidaten vermeidet, indem sie eine Äquivalenzbeziehung wählt und den Suchraum in Klassen äquivalenter Ausdrücke unterteilt. Diese Technik erweist sich als effizienter als bestehende Ansätze, wobei Experimente signifikante Beschleunigungen und die Fähigkeit zeigen, nicht realisierbare Synthesefälle effektiver zu erkennen. Das Kapitel stellt auch ein Synthesewerkzeug namens Polysemist vor, das die vorgeschlagene Methode implementiert und modernste Werkzeuge sowohl in realisierbaren als auch in nicht realisierbaren Syntheseproblemen übertrifft. Die Fähigkeit des Tools, ein komplettes TLA + -Protokoll von Grund auf in bemerkenswert kurzer Zeit zu synthetisieren, unterstreicht sein Potenzial für praktische Anwendungen im Design und in der Verifikation verteilter Systeme.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA+. Our method’s chief novelty lies in a new search space reduction technique called interpretation reduction, which allows to not only eliminate incorrect candidate protocols before they are sent to the verifier, but also to avoid enumerating redundant candidates in the first place. Further performance improvements are achieved by an advanced technique for exact generalization of counterexamples. Experiments on a set of established benchmarks show that our tool is almost always faster than the state of the art, often by orders of magnitude, and was also able to synthesize an entire TLA+ protocol “from scratch” in less than 3 minutes where the state of the art timed out after an hour. Our method is sound, complete, and guaranteed to terminate on unrealizable synthesis instances under common assumptions which hold in all our benchmarks. -
Synthesis of Universal Safety Controllers
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die Synthese universeller Sicherheitscontroller und überbrückt die Lücke zwischen reaktiver Synthese und aufsichtsrechtlicher Kontrolle. Es befasst sich mit den Beschränkungen traditioneller Methoden, die aufgrund der Notwendigkeit, alle möglichen Pflanzenverhaltungen in das Modell einzubeziehen, mit Skalierbarkeit zu kämpfen haben. Das Kapitel stellt einen bahnbrechenden Ansatz vor, der die Synthese eines universellen Controllers von seiner Anpassung an spezifische Anlagenmodelle entkoppelt, indem er Prophezeiungen verwendet, um Reglerleistungen auf Grundlage zukünftigen Anlagenverhaltens zu konditionieren. Diese Methode verbessert die Skalierbarkeit und Anpassungsfähigkeit und ermöglicht eine effiziente Synthese, selbst wenn das Pflanzenmodell nicht vollständig bekannt ist oder sich im Laufe der Zeit ändert. Das Kapitel bietet einen umfassenden Überblick über die theoretischen Grundlagen, einschließlich der formalen Einführung universeller Steuerungen und Prophezeiungen, und stellt einen Algorithmus zur Synthese universeller Steuerungen aus Sicherheitsspezifikationen vor. Es enthält auch experimentelle Ergebnisse, die die verbesserte Skalierbarkeit des Ansatzes im Vergleich zu Standardmethoden belegen. Das Kapitel schließt mit einer Diskussion der Vorteile universeller Steuerungen, einschließlich ihrer Anpassungsfähigkeit an neue Anlagen und dynamische Veränderungen, sowie ihrer Erklärbarkeit, die spezifische Anlageneigenschaften identifiziert, die bestimmte Steuerungen sicherer machen.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractThe goal of logical controller synthesis is to automatically compute a control strategy that regulates the discrete, event-driven behavior of a given plant s.t. a temporal logic specification holds over all remaining traces. Standard approaches to this problem construct a two-player game by composing a given complete plant model and the logical specification and applying standard algorithmic techniques to extract a control strategy. However, due to the often enormous state space of a complete plant model, this process can become computationally infeasible. In this paper, we introduce a novel synthesis approach that constructs a universal controller derived solely from the game obtained by the standard translation of the logical specification. The universal controller’s moves are annotated with prophecies – predictions about the plant’s behavior that ensure the move is safe. By evaluating these prophecies, the universal controller can be adapted to any plant over which the synthesis problem is realizable. This approach offers several key benefits, including enhanced scalability with respect to the plant’s size, adaptability to changes in the plant, and improved explainability of the resulting control strategy. We also present encouraging experimental results obtained with our prototype tool, unicon. -
Synthesis with Guided Environments
- Open Access
PDF-Version jetzt herunterladenDas Kapitel stellt das Konzept der Synthese mit geführten Umgebungen (SGE) vor, einem neuartigen Ansatz zur Systemsynthese, bei dem das System die Handlungen der Umwelt lenken kann. Diese Methode ist besonders in Szenarien mit teilweiser Sichtbarkeit vorteilhaft, in denen das System nicht alle Eingangssignale beobachten kann. Das Kapitel untersucht die technischen Herausforderungen und Vorteile von SGE, einschließlich der Zersetzung der Zufriedenheitsaufgabe zwischen dem System und der Umwelt. Es geht um den Speicher, der von der Umgebung genutzt wird und wie er optimiert werden kann, sowie um die automatisierungsbasierte Lösung für SGE. Das Kapitel behandelt auch den Bereich der Programme, die von den Wandlern mit geführten Umgebungen (TGEs) verwendet werden und wie diese effizient dargestellt werden können. Darüber hinaus vergleicht er den SGE-Ansatz mit traditionellen Synthesemethoden und verteilten Systemen und hebt die einzigartigen Vorteile und technischen Herausforderungen von SGE hervor. Das Kapitel endet mit Anweisungen für zukünftige Forschung, einschließlich dynamischer Ausblendung und Führung von Signalen und begrenzter SGE. Die detaillierte Analyse und die technische Tiefe machen dieses Kapitel zu einer wertvollen Ressource für Spezialisten, die fortgeschrittene Synthesetechniken verstehen und umsetzen wollen.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractIn the synthesis problem, we are given a specification, and we automatically generate a system that satisfies the specification in all environments. We introduce and study synthesis with guided environments (SGE, for short), where the system may harness the knowledge and computational power of the environment during the interaction. The underlying idea in SGE is that in many settings, in particular when the system serves or directs the environment, it is of the environment’s interest that the specification is satisfied, and it would follow the guidance of the system. Thus, while the environment is still hostile, in the sense that the system should satisfy the specification no matter how the environment assigns values to the input signals, in SGE the system assigns values to some output signals and guides the environment via programs how to assign values to other output signals. A key issue is that these assignments may depend on input signals that are hidden from the system but are known to the environment, using programs like “copy the value of the hidden input signal x to the output signal y.” SGE is thus particularly useful in settings where the system has partial visibility.We solve the problem of SGE, show its superiority with respect to traditional synthesis, and study theoretical aspects of SGE, like the complexity (memory and domain) of programs used by the system, as well as the connection of SGE to synthesis of (possibly distributed) systems with partial visibility. -
Value Iteration with Guessing for Markov Chains and Markov Decision Processes
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die Optimierung der Value Iteration (VI) für Markov-Ketten (MCs) und Markov-Entscheidungsprozesse (MDPs), wobei der Schwerpunkt auf der Verbesserung der Effizienz von VI durch innovative Vorverarbeitungstechniken liegt. Die Autoren stellen Guessing VI vor, einen neuartigen Ansatz, der die Anzahl der Bellman-Aktualisierungen, die für die Wertangleichung erforderlich sind, deutlich reduziert. Für MCs stellt das Kapitel einen fast linearen Vorverarbeitungsalgorithmus vor, der in Kombination mit Schätzwerten nur subexponentiell viele Bellman-Aktualisierungen erfordert. Dieser Ansatz ist symbolisch umsetzbar und zeigt wesentliche Verbesserungen gegenüber bestehenden Methoden. Das Kapitel weitet diese Technik auch auf MEPs aus und präsentiert eine neue Analyse der VI-Konvergenz und eine praktische Umsetzung namens Guessing VI. Experimentelle Ergebnisse zum Quantitativen Verifikationsbenchmark Set zeigen, dass Guessing VI in einer beträchtlichen Anzahl von Fällen bestehende VI-basierte Ansätze übertrifft, was sein Potenzial für praktische Anwendungen verdeutlicht. Das Kapitel behandelt auch verwandte Arbeiten und bietet einen umfassenden Überblick über die theoretischen Grundlagen und experimentellen Bewertungen, was es zu einer wertvollen Ressource für Forscher und Praktiker auf dem Gebiet der probabilistischen Verifikation und Optimierung macht.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractTwo standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.
-
-
Equivalence Checking
-
Frontmatter
-
Equivalence Checking of a libm Port
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die Überprüfung der Äquivalenz eines Rust-Ports der musl C Mathematik-Bibliothek, wobei der Schwerpunkt auf den Herausforderungen und Lösungen bei der Überprüfung der Korrektheit des portierten Codes liegt. Die Arbeit nutzt den SMACK-Softwareprüfer, der sowohl C als auch Rust unterstützt, um sicherzustellen, dass das Verhalten der ursprünglichen C-Bibliothek mit der Rust-Implementierung übereinstimmt. Das Kapitel vertieft sich in die Feinheiten der Fließkomma-Arithmetik, die durch Rundungen und spezielle Werte wie NaN zusätzliche Komplexitäten mit sich bringt. Es untersucht den Toolflow von SMACK und beschreibt, wie es den LLVM-IR-Code zur Verifikation mit Backend-Solvern wie Z3 und CVC5 in eine Boogie Intermediate Verifikationssprache übersetzt. In diesem Kapitel werden auch verschiedene Techniken zur Verbesserung der Skalierbarkeit von Verifikationen diskutiert, darunter eine übermäßige Annäherung von Theorien, die Einschränkung von Operationen zur Vermeidung von NaN-Werten und eine gesteuerte Äquivalenzprüfung. Praktische Experimente werden an einer Reihe von Benchmarks durchgeführt, die die Leistungsfähigkeit verschiedener Prüfer und die Entdeckung von Fehlern sowohl in der Rust-Bibliothek als auch im SMACK-Prüfer offenbaren. Das Kapitel schließt mit einer Diskussion über verwandte Arbeiten und das Potenzial für zukünftige Anwendungen der entwickelten Techniken.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractRecent advances in satisfiability modulo theories have brought practical software verification within reach. The advent of the LLVM project presents a common representation which allows verification between programs written in different languages such as C and Rust. New programming languages such as Rust often have less complete standard libraries. In this work, we explore using the SMACK software verifier to check the equivalence of math library routines from themusllibm library and their translations into native Rust programs. -
Revisiting Differential Verification: Equivalence Verification with Confidence
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht den kritischen Bereich der Äquivalenzüberprüfung neuronaler Netzwerke und konzentriert sich auf die Herausforderungen und Fortschritte bei der Gewährleistung, dass sich neue neuronale Netzwerke den etablierten Referenznetzen äquivalent verhalten. Es beginnt mit der Komplexität der Spezifizierung neuronaler Netzwerkverhalten und der relativ einfachen Formalisierung von Äquivalenzeigenschaften, die für verschiedene Anwendungen wie Umschulung, Schnitt und Schüler-Lehrer-Ausbildung von entscheidender Bedeutung sind. Der Text geht auf die theoretischen Grundlagen der Äquivalenzverifizierung ein und hebt die KoNP-Vollständigkeit der Top-1-Äquivalenzverifizierung hervor, eine bedeutende Erkenntnis, die bisher nicht etabliert wurde. Es werden Differentielle Zonotope eingeführt, ein innovativer abstrakter Bereich, der die Effizienz differentiellen Denkens bei der Äquivalenzüberprüfung verbessert. Diese Methode zeigt in Verbindung mit einer geeigneten Verfeinerung heuristischer und Generatorkompressionstechniken eine überlegene Leistung gegenüber bestehenden Ansätzen. Das Kapitel schlägt außerdem eine vertrauensbasierte Klassifikationsäquivalenzeigenschaft vor, die eine Überprüfung über größere Teile des Eingabebereichs ermöglicht. Diese Eigenschaft nutzt die Vertrauenswerte, die durch neuronale Netzwerke der Klassifikation bereitgestellt werden, und bietet einen globaleren und praktischeren Ansatz zur Überprüfung der Äquivalenz. Der Evaluierungsbereich zeigt die Umsetzung dieser Methoden in einem neuen Tool, VeryDiff, das erhebliche Beschleunigungen erzielt und in verschiedenen Benchmark-Szenarien modernste Prüfer übertrifft. Das Kapitel schließt mit einer Diskussion über die Beschränkungen und zukünftigen Richtungen der differentiellen Verifikation und betont ihr Potenzial, den Bereich der Verifikation neuronaler Netzwerke zu revolutionieren.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWhen validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the (original) reference NN. To this end, our paper revisits the idea of differential verification which performs reasoning on differences between NNs: On the one hand, our paper proposes a novel abstract domain for differential verification admitting more efficient reasoning about equivalence. On the other hand, we investigate empirically and theoretically which equivalence properties are (not) efficiently solved using differential reasoning. Based on the gained insights, and following a recent line of work on confidence-based verification, we propose a novel equivalence property that is amenable to Differential Verification while providing guarantees for large parts of the input space instead of small-scale guarantees constructed w.r.t. predetermined input points. To this end, we propose an improved approach for (approximately) constraining an NN’s softmax confidence. We implement our approach in a new tool called VeryDiff and perform an extensive evaluation on numerous old and new benchmark families, including new pruned NNs for particle jet classification in the context of CERN’s LHC where we observe median speedups \(>300\times \) over the State-of-the-Art verifier \(\alpha ,\beta \)-CROWN. -
Refuting Equivalence in Probabilistic Programs with Conditioning
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die schwierige Aufgabe, Äquivalenz in probabilistischen Programmen (PPs) zu widerlegen, die Konditionierung beinhalten. PPs, die Standardprogramme um probabilistische Anweisungen erweitern, sind in verschiedenen Bereichen wie Vernetzung, Datenschutz, Sicherheit und Robotik weit verbreitet. Das Kapitel stellt eine bahnbrechende Methode zum Nachweis der Ungleichheit bedingter Produktionsverteilungen in ÖPP mit Konditionierung vor, ein Problem, das bis heute größtenteils ungelöst ist. Die Methode ist vollautomatisiert, anwendbar auf unendliche, diskrete und kontinuierliche Turing-vollständige PPs und liefert nachweislich korrekte Widerlegungen. Es baut auf den Vorstellungen von Supermartingalen (U / LESM) auf und führt das Konzept eines gewichteten Neustarts ein, um ÖPPs mit Konditionierung in konditionierungsfreie ÖPPs zu übersetzen. Das Kapitel stellt auch Garantien für die Solidität und Vollständigkeit der Beweisregel auf der Grundlage von U / LESM vor, ein neuartiges Ergebnis auf diesem Gebiet. Darüber hinaus enthält sie eine experimentelle Bewertung, die die Überlegenheit der Methode gegenüber bestehenden Baselines hinsichtlich der Anzahl der widerlegten Äquivalenzen belegt. Das Kapitel berührt auch die potenzielle Anwendung eines gewichteten Neustarts auf Ähnlichkeitswiderlegungen in ÖPP mit Konditionierung, was den Weg für zukünftige Forschungen in diesem Bereich ebnet.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.
-
-
Games
-
Frontmatter
-
Non-Zero-Sum Games with Multiple Weighted Objectives
- Open Access
PDF-Version jetzt herunterladenDas Kapitel untersucht die Synthese von Strategien in Multiplayer-Spielen mit gewichteten Zielen, wobei der Schwerpunkt auf der Interaktion von Komponenten in modernen Systemen liegt. Es stellt das Konzept der MaxWB-Spiele vor, bei denen jeder Spieler ein gewichtetes mehrfaches Büchi-Ziel hat, und untersucht die Stabilität und das Gleichgewicht dieser Spiele. Das Kapitel geht der Komplexität der Suche nach stabilen Profilen nach, die die gewünschten Eigenschaften erfüllen, wobei verschiedene Einschränkungen der Gewichtsfunktionen und deren Auswirkungen auf die Ausdruckskraft und Komplexität der Spiele berücksichtigt werden. Es führt auch das Konzept der Spiele mit Zahlungen ein, bei denen die Spieler einander Anreize geben können, vorteilhafte Strategien zu verfolgen. Das Kapitel bietet eine umfassende Analyse des DNE-Problems und bietet Einblicke in die Synthese von Strategien in Spielen mit Zahlungen und die monetäre Reparatur von Systemen. Es wird auch die Anwendung von MaxWB-Spielen in verschiedenen Umgebungen diskutiert, wie etwa Roboter, die ein Lager patrouillieren und Supercomputer, die Kalkulationsanfragen bearbeiten, wobei die praktische Relevanz der diskutierten Konzepte hervorgehoben wird.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe introduce and study non-zero-sum multi-player games with weighted multiple objectives. In these games, the objective of each player consists of a set \(\alpha \) of underlying objectives and a weight function \(w: 2^\alpha \rightarrow \mathbb {Z}\) that maps each subset X of \(\alpha \) to the utility of the player when exactly all the objectives in X are satisfied.We study the existence and synthesis of stable outcomes with desired utilities for the players. The problem generalizes rational synthesis and enables the synthesis of outcomes that satisfy wellness, fairness, and priority requirements.We study the extension of the game by payments, with which players can incentivize each other to follow strategies that are beneficial for the paying player. We show how such payments can be used in order to repair systems. We study the complexity of the setting for various classes of weight functions. In particular, general weight functions are related to Muller objectives, and the synthesis problem for them is PSPACE-complete. We study non-decreasing, additive, positive, and other classes of weight functions, and the way they affect the memory required for the players and the complexity of the synthesis problem. -
Fast value iteration: A uniform approach to efficient algorithms for energy games
- Open Access
PDF-Version jetzt herunterladenDas Kapitel untersucht die effiziente Berechnung von Energiewerten in Spielen mit endloser Dauer, in denen zwei Spieler, Min und Max, durch eine endlich gerichtete Grafik navigieren, um ihre Auszahlungen zu optimieren. Es führt einen einheitlichen Ansatz zur schnellen Wertwiederholung ein, der bestehende Algorithmen vereinheitlicht und vereinfacht und eine systematische Methode zur Herstellung effizienter Löser bereitstellt. Der Text vertieft sich in die theoretischen Grundlagen von Energie- und Mean-Paid-Spielen und hebt die Positionsbestimmung hervor, die es den Spielern erlaubt, Strategien anzuwenden, die nur von der aktuellen Spielposition abhängig sind. Es werden verschiedene algorithmische Paradigmen diskutiert, darunter Wertwiederholungen und Strategieverbesserungen, und hybride Algorithmen eingeführt, die Elemente aus beiden kombinieren. Das Kapitel stellt ein auf potenziellen Verringerungen basierendes Rahmenwerk für die schnelle Iteration von Werten vor, das Zyklusgewichte und mittlere Auszahlungswerte beibehält und so die Korrektheit der daraus abgeleiteten Algorithmen sicherstellt. Es untersucht und vereinheitlicht bestehende Algorithmen wie OSI und QDPM und schlägt neue Algorithmen wie Positive Path Iteration (PPI) und ihre dynamische Variante (DPPI) vor. Die empirische Bewertung vergleicht diese Algorithmen mit Paritätslösern der Spitzenklasse und demonstriert deren Effizienz und Robustheit, insbesondere im Umgang mit harten Instanzen. Das Kapitel schließt mit einer Diskussion offener Fragen und zukünftiger Forschungsrichtungen, wobei das Potenzial für weitere Verbesserungen und neue algorithmische Entwicklungen betont wird.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractWe study algorithms for solving parity, mean-payoff and energy games. We propose a systematic framework, which we call Fast value iteration, for describing, comparing, and proving correctness of such algorithms. The approach is based on potential reductions, as introduced by Gurvich, Karzanov and Khachiyan (1988). This framework allows us to provide simple presentations and correctness proofs of known algorithms, unifying the Optimal strategy improvement algorithm by Schewe (2008) and the quasi dominions approach by Benerecetti et al. (2020), amongst others. The new approach also leads to novel symmetric versions of these algorithms, highly efficient in practice, but for which we are unable to prove termination. We report on empirical evaluation, comparing the different fast value iteration algorithms, and showing that they are competitive even to top parity game solvers. -
Proxy Attribute Discovery in Machine Learning Datasets via Inductive Logic Programming
- Open Access
PDF-Version jetzt herunterladenDieses Kapitel untersucht die entscheidende Frage der Fairness im maschinellen Lernen, indem es sich auf die Erkennung von Stellvertreterattributen konzentriert, die zu indirekter Diskriminierung führen können. Es führt eine bahnbrechende Methodik ein, die die induktive Logik-Programmierung (ILP) nutzt, um Stellvertreterattribute in Trainingsdatensätzen zu identifizieren und damit die Fairness von KI-Modellen zu verbessern. Das Kapitel bietet einen eingehenden Vergleich des ILP mit traditionellen kausalen Ansätzen, hebt die Vorteile des ILP im Umgang mit verrauschten Daten hervor, unterstützt arithmetische Beziehungen und erfordert minimales Domänenwissen. Es präsentiert auch ein praktisches Python-Tool, PADTAI, das erfolgreich auf Datensätze aus der realen Welt angewendet wurde und bis zu 83 Proxy-Beziehungen aufdeckt. Das Kapitel vertieft sich in die Bewertung des Tools, diskutiert die Stärken und Grenzen des Ansatzes und bietet Einblicke in die Interpretation und Validierung der erkannten Proxy-Beziehungen. Durch die Bewältigung der Herausforderungen bei der Entdeckung von Stellvertreterattributen trägt dieses Kapitel erheblich zu den laufenden Bemühungen bei, Fairness bei KI und maschinellem Lernen zu gewährleisten.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractThe issue of fairness is a well-known challenge in Machine Learning (ML) that has gained increased importance with the emergence of Large Language Models (LLMs) and generative AI. Algorithmic bias can manifest during the training of ML models due to the presence of sensitive attributes, such as gender or racial identity. One approach to mitigate bias is to avoid making decisions based on these protected attributes. However, indirect discrimination can still occur if sensitive information is inferred from proxy attributes. To prevent this, there is a growing interest in detecting potential proxy attributes before training ML models. In this case study, we report on the use of Inductive Logic Programming (ILP) to discover proxy attributes in training datasets, with a focus on the ML classification problem. While ILP has established applications in program synthesis and data curation, we demonstrate that it can also advance the state of the art in proxy attribute discovery by removing the need for prior domain knowledge. Our evaluation shows that this approach is effective at detecting potential sources of indirect discrimination, having successfully identified proxy attributes in several well-known datasets used in fairness-awareness studies. -
Reachability for Nonsmooth Systems with Lexicographic Jacobians
- Open Access
PDF-Version jetzt herunterladenDas Kapitel vertieft die Komplexität der Erreichbarkeitsanalyse für nichtglatte dynamische Systeme, die durch kontinuierliche, aber nicht differenzierbare Funktionen gekennzeichnet sind. Traditionelle Methoden haben mit diesen Systemen zu kämpfen, weil es an nicht differenzierbaren Punkten keine klar definierten Jakobiner gibt, was zu konservativen Übernäherungen führt. Die Autoren schlagen einen bahnbrechenden Algorithmus vor, der lexikographische Differenzierung zur Berechnung direktionaler Derivate nutzt und wertvolle Informationen erster Ordnung selbst an nicht differenzierbaren Punkten liefert. Dieser Ansatz umgeht die Notwendigkeit einer expliziten Berechnung erreichbarer Grenzwerte, eine bedeutende Barriere in der hybriden Erreichbarkeitsanalyse. Der Algorithmus wird durch experimentelle Ergebnisse an 12 nicht glatten dynamischen Benchmark-Modellen validiert, die eine bis zu 4-mal höhere Genauigkeit aufweisen als hochmoderne Werkzeuge wie CORA und JuliaReach. Das Kapitel untersucht auch die Anwendung dieser Methode auf neuronale ODEs der ReLU, einer besonders herausfordernden Klasse nichtglatter Systeme, und demonstriert ihr Potenzial, die Erreichbarkeitsanalyse komplexer dynamischer Systeme voranzutreiben.KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
AbstractReachability analysis for dynamical systems typically relies on the system’s Jacobian to bound sensitivity of solutions. This method fails for nonsmooth dynamical systems as the Jacobian becomes undefined at the points where the vector field is non-differentiable. Such models can be hybridized by gluing together several smooth subsystems or modes via transitions, but the accuracy of reachability degrades when reachable sets are propagated across the mode boundaries. We propose an alternative approach based on lexicographic differentiation. Lexicographic differentiation was introduced by Nesterov as a foundation for calculus for nonsmooth functions. Our algorithm computes linear bounds on sets of lexicographic Jacobians, which give bounds on trajectory sensitivities. This avoids hybridization, eliminates mode transition computations, and yields more accurate reachsets. On nonsmooth models, our method improves accuracy on average by 50%, compared to hybrid algorithms. It is also one of the first methods to effectively handle reachability of ReLU neural ODEs.
-
- Titel
- Tools and Algorithms for the Construction and Analysis of Systems
- Herausgegeben von
-
Arie Gurfinkel
Marijn Heule
- Copyright-Jahr
- 2025
- Verlag
- Springer Nature Switzerland
- Electronic ISBN
- 978-3-031-90653-4
- Print ISBN
- 978-3-031-90652-7
- DOI
- https://doi.org/10.1007/978-3-031-90653-4
Informationen zur Barrierefreiheit für dieses Buch folgen in Kürze. Wir arbeiten daran, sie so schnell wie möglich verfügbar zu machen. Vielen Dank für Ihre Geduld.
