{"id":{"repo_id":"freiburg-diss","oai_identifier":"oai:freidok.uni-freiburg.de:1234"},"canonical_url":"https://search.dev.ndltd.org/etd/freiburg-diss/oai:freidok.uni-freiburg.de:1234","repository":{"repo_id":"freiburg-diss","name":"University of Freiburg","base_url":"https://freidok.uni-freiburg.de/oai/oai2.php"},"display":{"title":"System verification tools based on Monadic Logics","abstract":"In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den ausdrucksstärksten Logiken, die noch entscheidbar sind. Gegenwärtig werden monadische Logiken auch in der Informatik zum Zweck der formalen Systemverifikation verwendet. Entscheidungsverfahren für diese Logiken wurden in verschiedenen Werkzeugen wie z.B. Mona, MOSEL und dem Step System implementiert und teilweise erfolgreich in unterschiedlichen Anwendungsgebieten, vor allem in der Hardware- und Protokoll-verifikation, eingesetzt.
Der Erfolg der auf monadischen Logiken basierten Verifikationswerkzeuge wird allerdings durch zwei große Nachteile, die diese Logiken mit sich bringen, erheblich vermindert. Zum einen sind diese Logiken wegen ihres geringen Abstraktionsgrades als Spezifikationssprachen ungeeignet; die Formalisierung von Systemen und Systemeigenschaften in diesen Logiken bedarf eines hohen Maßes an Erfahrung und Detailkenntnissen und ist mit der Programmierung in Assembler vergleichbar. Zum anderen haben die Entscheidungsverfahren für diese Logiken eine sehr hohe Berechnungskomplexität; oft brechen die oben genannten Werkzeuge ihre Berechnung aus Mangel an Speicherressourcen ab.
Die vorliegende Arbeit stellt mehrere Verfahren vor, die die erwähnten Nachteile überwinden und machen somit die monadischen Logiken für die Praxis besser nutzbar. Nachfolgend stellen wir die Beiträge in unserer Arbeit dar. Wir entwickeln zunächst eine neue auf monadische Logik über endliche Bäume basierende Spezifikationssprache, die intuitiv und benutzerfreundlich ist und Sprachkonstrukte bereitstellt, die einen höheren Abstraktionsgrad ermöglichen. Außerdem geben wir eine syntaktische Charakterisierung von Klassen von Formeln der neu entwickelten Spezifikationssprache an, die eine akzeptable Berechungskomplexität haben.
Desweiteren untersuchen wir das Problem der sogenannten Zustandsraumexplosion: Bei der Verifikation von großen Systemen in monadischen Logiken kann der Zustandsraum nicht-elementar groß werden. Um dieses Problem zu vermeiden, geben wir ein Verfahren an, das für die Generierung von Gegenbeispielen eine effektive und nicht-elementare Verbesserung gegenüber den herkömmlichen Entscheidungsverfahren bietet.
Schließlich beschäftigen wir uns auch mit der Frage, wie man, ausgehend von der Kernidee dieser Methode zur Generierung von Gegenbeispielen, monadische Logiken über endlichen Wörtern zum Nachweis von Eigenschaften nicht-terminierender Systeme benutzen kann.
Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch Lebendigkeitseigenschaften in monadischen Logiken über endlichen Wörtern formalisieren und dadurch automatisch beweisen kann.
Die Praxistauglichkeit unserer theoretischen Resultate stellen wir durch die Implementierung von verschiedenen Verifikationswerkzeugen (Lisa, Monaco und Qubos) unter Beweis. Anwendbarkeit und Skalierbarkeit dieser Werkzeuge werden anhand nicht-trivialer Fallbeispiele evaluiert.","abstract_html":"In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den ausdrucksstärksten Logiken, die noch entscheidbar sind. Gegenwärtig werden monadische Logiken auch in der Informatik zum Zweck der formalen Systemverifikation verwendet. Entscheidungsverfahren für diese Logiken wurden in verschiedenen Werkzeugen wie z.B. Mona, MOSEL und dem Step System implementiert und teilweise erfolgreich in unterschiedlichen Anwendungsgebieten, vor allem in der Hardware- und Protokoll-verifikation, eingesetzt. <br>Der Erfolg der auf monadischen Logiken basierten Verifikationswerkzeuge wird allerdings durch zwei große Nachteile, die diese Logiken mit sich bringen, erheblich vermindert. Zum einen sind diese Logiken wegen ihres geringen Abstraktionsgrades als Spezifikationssprachen ungeeignet; die Formalisierung von Systemen und Systemeigenschaften in diesen Logiken bedarf eines hohen Maßes an Erfahrung und Detailkenntnissen und ist mit der Programmierung in Assembler vergleichbar. Zum anderen haben die Entscheidungsverfahren für diese Logiken eine sehr hohe Berechnungskomplexität; oft brechen die oben genannten Werkzeuge ihre Berechnung aus Mangel an Speicherressourcen ab.<br>Die vorliegende Arbeit stellt mehrere Verfahren vor, die die erwähnten Nachteile überwinden und machen somit die monadischen Logiken für die Praxis besser nutzbar. Nachfolgend stellen wir die Beiträge in unserer Arbeit dar. Wir entwickeln zunächst eine neue auf monadische Logik über endliche Bäume basierende Spezifikationssprache, die intuitiv und benutzerfreundlich ist und Sprachkonstrukte bereitstellt, die einen höheren Abstraktionsgrad ermöglichen. Außerdem geben wir eine syntaktische Charakterisierung von Klassen von Formeln der neu entwickelten Spezifikationssprache an, die eine akzeptable Berechungskomplexität haben. <br>Desweiteren untersuchen wir das Problem der sogenannten Zustandsraumexplosion: Bei der Verifikation von großen Systemen in monadischen Logiken kann der Zustandsraum nicht-elementar groß werden. Um dieses Problem zu vermeiden, geben wir ein Verfahren an, das für die Generierung von Gegenbeispielen eine effektive und nicht-elementare Verbesserung gegenüber den herkömmlichen Entscheidungsverfahren bietet.<br>Schließlich beschäftigen wir uns auch mit der Frage, wie man, ausgehend von der Kernidee dieser Methode zur Generierung von Gegenbeispielen, monadische Logiken über endlichen Wörtern zum Nachweis von Eigenschaften nicht-terminierender Systeme benutzen kann.<br>Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch Lebendigkeitseigenschaften in monadischen Logiken über endlichen Wörtern formalisieren und dadurch automatisch beweisen kann.<br>Die Praxistauglichkeit unserer theoretischen Resultate stellen wir durch die Implementierung von verschiedenen Verifikationswerkzeugen (Lisa, Monaco und Qubos) unter Beweis. Anwendbarkeit und Skalierbarkeit dieser Werkzeuge werden anhand nicht-trivialer Fallbeispiele evaluiert.","abstract_has_math":false,"creators":["Ayari, Abdelwaheb"],"institution":null,"degree_name":null,"degree_level":null,"degree_discipline":null,"degree_department":null,"school":null,"contributors":["Basin, David"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":null,"date_issued":"","date_published":null,"updated_at":"2026-07-24T02:22:03Z","subjects":["model checking","bounded model checking","sat solvers","decidable logics"],"languages":[],"rights":[],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"https://freidok.uni-freiburg.de/data/1234","outbound_label":"Repository record","outbound_source":"source_url"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Basin, David"]},{"key":"dc:creator","label":"Author","values":["Ayari, Abdelwaheb"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:type","label":"Dc Type","values":["DoctoralThesis"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["model checking","bounded model checking","sat solvers","decidable logics"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den ausdrucksstärksten Logiken, die noch entscheidbar sind. Gegenwärtig werden monadische Logiken auch in der Informatik zum Zweck der formalen Systemverifikation verwendet. Entscheidungsverfahren für diese Logiken wurden in verschiedenen Werkzeugen wie z.B. Mona, MOSEL und dem Step System implementiert und teilweise erfolgreich in unterschiedlichen Anwendungsgebieten, vor allem in der Hardware- und Protokoll-verifikation, eingesetzt.
Der Erfolg der auf monadischen Logiken basierten Verifikationswerkzeuge wird allerdings durch zwei große Nachteile, die diese Logiken mit sich bringen, erheblich vermindert. Zum einen sind diese Logiken wegen ihres geringen Abstraktionsgrades als Spezifikationssprachen ungeeignet; die Formalisierung von Systemen und Systemeigenschaften in diesen Logiken bedarf eines hohen Maßes an Erfahrung und Detailkenntnissen und ist mit der Programmierung in Assembler vergleichbar. Zum anderen haben die Entscheidungsverfahren für diese Logiken eine sehr hohe Berechnungskomplexität; oft brechen die oben genannten Werkzeuge ihre Berechnung aus Mangel an Speicherressourcen ab.
Die vorliegende Arbeit stellt mehrere Verfahren vor, die die erwähnten Nachteile überwinden und machen somit die monadischen Logiken für die Praxis besser nutzbar. Nachfolgend stellen wir die Beiträge in unserer Arbeit dar. Wir entwickeln zunächst eine neue auf monadische Logik über endliche Bäume basierende Spezifikationssprache, die intuitiv und benutzerfreundlich ist und Sprachkonstrukte bereitstellt, die einen höheren Abstraktionsgrad ermöglichen. Außerdem geben wir eine syntaktische Charakterisierung von Klassen von Formeln der neu entwickelten Spezifikationssprache an, die eine akzeptable Berechungskomplexität haben.
Desweiteren untersuchen wir das Problem der sogenannten Zustandsraumexplosion: Bei der Verifikation von großen Systemen in monadischen Logiken kann der Zustandsraum nicht-elementar groß werden. Um dieses Problem zu vermeiden, geben wir ein Verfahren an, das für die Generierung von Gegenbeispielen eine effektive und nicht-elementare Verbesserung gegenüber den herkömmlichen Entscheidungsverfahren bietet.
Schließlich beschäftigen wir uns auch mit der Frage, wie man, ausgehend von der Kernidee dieser Methode zur Generierung von Gegenbeispielen, monadische Logiken über endlichen Wörtern zum Nachweis von Eigenschaften nicht-terminierender Systeme benutzen kann.
Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch Lebendigkeitseigenschaften in monadischen Logiken über endlichen Wörtern formalisieren und dadurch automatisch beweisen kann.
Die Praxistauglichkeit unserer theoretischen Resultate stellen wir durch die Implementierung von verschiedenen Verifikationswerkzeugen (Lisa, Monaco und Qubos) unter Beweis. Anwendbarkeit und Skalierbarkeit dieser Werkzeuge werden anhand nicht-trivialer Fallbeispiele evaluiert.","Fundamental work on monadic second-order logics began about forty
years ago. These logics are amongst the most expressive logics that
are known to be decidable. Their first application domain was
mathematics, where they were for example used to decide theories of
arithmetics. Recently, they have also been applied to formally reason
about a number of problems in computer science: despite their
non-elementary complexity, decision procedures for monadic logics over
finite words and finite trees have been implemented in numerous tools
(eg, Mona, MOSEL, and Step) and have been successfully
applied to problems such as the verification of hardware and software
systems. These logics suffer, however, from two drawbacks that
strongly limit their application, namely the low-level language they
provide to specify systems and properties, and the demanding
computational complexity of their decision procedures.
To make system verification based on monadic logics more viable in
practice, in this thesis we systematically address both these problems
at once. To this end, we first improve the existing approaches (i) by
formalizing a new specification language which is expressive,
intuitive and more user-friendly, and (ii) by providing a handle on
the complexity of the logics' decision procedures. Second, we develop
new efficient algorithms and approaches to cope with the state-space
explosion problem. Third, we investigate how to employ the monadic
logic over finite words to reason about non-terminating systems.
Finally, we implement our methods in three tools (Lisa, Monaco,
and Qubos) and show their applicability and scalability."]},{"key":"dc:format.medium","label":"Dc Format Medium","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["System verification tools based on Monadic Logics","Werkzeuge zur Systemverifikation basierend auf monadischen Logiken"]}]}],"canonical_facts":{"dc:contributor":["Basin, David"],"dc:creator":["Ayari, Abdelwaheb"],"dc:description.abstract":["In der Mitte des letzten Jahrhunderts erschienen die ersten Arbeiten über monadische Logiken zweiter Stufe. Das Interesse an diesen Logiken lag zunächst hauptsächlich an Entscheidbarkeitsfragen von arithmetischen Theorien. Die monadischen Logiken zweiter Stufe über Wörter und Bäume gehören zu den ausdrucksstärksten Logiken, die noch entscheidbar sind. Gegenwärtig werden monadische Logiken auch in der Informatik zum Zweck der formalen Systemverifikation verwendet. Entscheidungsverfahren für diese Logiken wurden in verschiedenen Werkzeugen wie z.B. Mona, MOSEL und dem Step System implementiert und teilweise erfolgreich in unterschiedlichen Anwendungsgebieten, vor allem in der Hardware- und Protokoll-verifikation, eingesetzt.
Der Erfolg der auf monadischen Logiken basierten Verifikationswerkzeuge wird allerdings durch zwei große Nachteile, die diese Logiken mit sich bringen, erheblich vermindert. Zum einen sind diese Logiken wegen ihres geringen Abstraktionsgrades als Spezifikationssprachen ungeeignet; die Formalisierung von Systemen und Systemeigenschaften in diesen Logiken bedarf eines hohen Maßes an Erfahrung und Detailkenntnissen und ist mit der Programmierung in Assembler vergleichbar. Zum anderen haben die Entscheidungsverfahren für diese Logiken eine sehr hohe Berechnungskomplexität; oft brechen die oben genannten Werkzeuge ihre Berechnung aus Mangel an Speicherressourcen ab.
Die vorliegende Arbeit stellt mehrere Verfahren vor, die die erwähnten Nachteile überwinden und machen somit die monadischen Logiken für die Praxis besser nutzbar. Nachfolgend stellen wir die Beiträge in unserer Arbeit dar. Wir entwickeln zunächst eine neue auf monadische Logik über endliche Bäume basierende Spezifikationssprache, die intuitiv und benutzerfreundlich ist und Sprachkonstrukte bereitstellt, die einen höheren Abstraktionsgrad ermöglichen. Außerdem geben wir eine syntaktische Charakterisierung von Klassen von Formeln der neu entwickelten Spezifikationssprache an, die eine akzeptable Berechungskomplexität haben.
Desweiteren untersuchen wir das Problem der sogenannten Zustandsraumexplosion: Bei der Verifikation von großen Systemen in monadischen Logiken kann der Zustandsraum nicht-elementar groß werden. Um dieses Problem zu vermeiden, geben wir ein Verfahren an, das für die Generierung von Gegenbeispielen eine effektive und nicht-elementare Verbesserung gegenüber den herkömmlichen Entscheidungsverfahren bietet.
Schließlich beschäftigen wir uns auch mit der Frage, wie man, ausgehend von der Kernidee dieser Methode zur Generierung von Gegenbeispielen, monadische Logiken über endlichen Wörtern zum Nachweis von Eigenschaften nicht-terminierender Systeme benutzen kann.
Unsere Resultate ergeben, daß man sowohl Sicherheits- als auch Lebendigkeitseigenschaften in monadischen Logiken über endlichen Wörtern formalisieren und dadurch automatisch beweisen kann.
Die Praxistauglichkeit unserer theoretischen Resultate stellen wir durch die Implementierung von verschiedenen Verifikationswerkzeugen (Lisa, Monaco und Qubos) unter Beweis. Anwendbarkeit und Skalierbarkeit dieser Werkzeuge werden anhand nicht-trivialer Fallbeispiele evaluiert.","Fundamental work on monadic second-order logics began about forty
years ago. These logics are amongst the most expressive logics that
are known to be decidable. Their first application domain was
mathematics, where they were for example used to decide theories of
arithmetics. Recently, they have also been applied to formally reason
about a number of problems in computer science: despite their
non-elementary complexity, decision procedures for monadic logics over
finite words and finite trees have been implemented in numerous tools
(eg, Mona, MOSEL, and Step) and have been successfully
applied to problems such as the verification of hardware and software
systems. These logics suffer, however, from two drawbacks that
strongly limit their application, namely the low-level language they
provide to specify systems and properties, and the demanding
computational complexity of their decision procedures.
To make system verification based on monadic logics more viable in
practice, in this thesis we systematically address both these problems
at once. To this end, we first improve the existing approaches (i) by
formalizing a new specification language which is expressive,
intuitive and more user-friendly, and (ii) by providing a handle on
the complexity of the logics' decision procedures. Second, we develop
new efficient algorithms and approaches to cope with the state-space
explosion problem. Third, we investigate how to employ the monadic
logic over finite words to reason about non-terminating systems.
Finally, we implement our methods in three tools (Lisa, Monaco,
and Qubos) and show their applicability and scalability."],"dc:format.medium":["application/pdf"],"dc:subject":["model checking","bounded model checking","sat solvers","decidable logics"],"dc:title":["System verification tools based on Monadic Logics","Werkzeuge zur Systemverifikation basierend auf monadischen Logiken"],"dc:type":["DoctoralThesis"]},"updated_at":"2026-07-24T02:22:03Z"}