In dieser Arbeit wird die Verwendung eingeschränkter polynomialer logischer Zonotope für die formale Verifikation logischer Systeme vorgeschlagen. Durch Erreichbarkeitsanalyse wird die Menge der erreichbaren Zustände berechnet, um zu überprüfen, ob unerwünschte Zustände erreicht werden können.
Polynomiale logische Zonotope sind eine kürzlich eingeführte Darstellung, die eine effiziente und exakte Erreichbarkeitsanalyse logischer Systeme ermöglicht. Allerdings unterstützen polynomiale logische Zonotope keine exakten Schnittoperationen, was für die formale Verifikation erforderlich ist.
Um dieses Problem zu lösen, werden in dieser Arbeit eingeschränkte polynomiale logische Zonotope eingeführt. Diese Darstellung behält die Vorteile polynomialer logischer Zonotope bei und ermöglicht zusätzlich exakte Schnittoperationen. Es werden die verschiedenen Mengenoperationen auf eingeschränkten polynomialen logischen Zonotopen hergeleitet, einschließlich exakter Schnittoperationen, Minkowski-Operationen und exakter logischer Operationen.
Abschließend wird die Anwendung eingeschränkter polynomialer logischer Zonotope für die Erreichbarkeitsanalyse und Schnittoperationen evaluiert und mit anderen Darstellungen verglichen. Die Ergebnisse zeigen, dass eingeschränkte polynomiale logische Zonotope eine effiziente und exakte Lösung für die formale Verifikation logischer Systeme bieten.
A otro idioma
del contenido fuente
arxiv.org
Ideas clave extraídas de
by Ahmad Hafez,... a las arxiv.org 03-28-2024
https://arxiv.org/pdf/2403.18564.pdfConsultas más profundas