Verifikation nicht-regulärer Eigenschaften

• Applicant: Professor Dr. Martin Lange
• Subject Area: Theoretical Computer Science
• Term: from 2005 to 2010
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 16789390

• Final Report Year: 2010

Final Report Abstract

Aufgabe der automatischen Programmverifikation ist es, zu einem gegebenen Programm und einer gegebenen Eigenschaft statisch zu verifizieren, ob das Programm diese Eigenschaft besitzt. Lösungen für dieses Problem stellen sehr wichtige Mittel dar, um die Zuverlässigkeit sicherheitskritischer Hard- und Software zu garantieren. Eine mittlerweile etablierte Methode in der Programmverifikation ist Model Checking. Sie wird seit mehr als 25 Jahren betrieben und hält auch immer mehr Einzug in die industrielle a Entwicklung von Hard- und Software. Dabei lag der Fokus jedoch bisher hauptsächlich auf sehr ausdrucksschwachen Spezifikationssprachen für Korrektheitseigenschaften. Ziel des Projekts “Verifikation nicht-regulärer Eigenschaften” war es, den Bereich der Programmeigenschaften, die automatisch, insbesondere durch Model Checking überprüft werden können, um komplexere Eigenschaften zu erweitern, um somit in gewissem Sinne mehr Verifikation zu ermöglichen. Dazu wurden u.a. ausdrucksstarke Temporallogiken in Hinblick auf die Komplexität ihrer Model-Checkig-Probleme und ihre relative Ausdrucksstärken zueinander hin untersucht. Die so entstehende Hierarchie dieser Spezifikationssprachen klassifiziert u.a. Programmeigenschaften nach der Schwierigkeit, sie zu verifizieren und strukturiert erstmals den Raum der Programmeigenschaften, die nicht mehr im bisher wohl-verstandenen Bereich der sogenannten regulären (und damit recht einfachen) Programmeigenschaften liegen. Desweiteren wurden konkrete Model-Checking-Algorithmen für existierende und neu definierte Logiken entworfen und teilweise auch prototypisch implementiert. Während sich die Anträge zu diesem Projekt noch hauptsächlich auf die Verwendung ausdrucksstarker Temporallogiken im Bereich der Programmverifikation konzentriert haben, hat sich im Laufe des Projekts gezeigt, dass diese auch in anderen Gebieten innerhalb der Informatik aufgrund ihrer hohen Ausdrucksstärke beim Lösen anderer Probleme zur Anwendung kommen können. So konnten Algorithmen für interessante Probleme im Bereich der Theorie formaler Sprachen bzw. der Bio-Informatik mithilfe von Model-Checking-Techniken für solche Logiken gefunden werden. Desweiteren hat sich im Verlaufe der Arbeiten an solchen Logiken auch innerhalb des Bereichs der automatischen Programmverifikation eine weitere Verwendungsmöglichkeit aufgetan. Solche Logiken können u.U. eingesetzt werden, um auf präzisere Weise Verifikation von Programmen mit unendlichen Zustandsräumen zu betreiben. Dazu kann die Information, die durch die Abstraktion auf seiten des zugrundeliegenden Systems verloren geht, teilweise durch die hohe Ausdrucksstärke der verwendeten Logik in der Formel aufgefangen werden.

Publications

• Model checking propositional dynamic logic with all extras. Journal of Applied Logic, 4(1):39–49, 2005.
  M. Lange
  
• Temporal logics for non-regular properties: Model checking. In H. Schlingloff, editor, Proc. 4th Int. Workshop on Methods for Modalities, M4M-4, volume 194 of Informatik Berichte, pages 1–7, Berlin, Germany, 2005. HU Berlin.
  M. Lange
  
• The complexity of model checking higher order fixpoint logic. In Proc. 30th Int. Symp. on Math. Foundations of Computer Science, MFCS’05, volume 3618 of LNCS, pages 640–651. Springer, 2005
  M. Lange and R. Somla
  
• Propositional dynamic logic of context-free programs and fixpoint logic with chop. Information Processing Letters, 100(2):72–75, 2006
  M. Lange and R. Somla
  
• The alternation hierarchy in fixpoint logic with chop is strict too. Information and Computation, 204(9):1346–1367, 2006.
  M. Lange
  
• Model checking the first-order fragment of higher-order fixpoint logic. In Proc. 14th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR’07, volume 4790 of LNCS, pages 62–76. Springer, 2007.
  R. Axelsson and M. Lange
  
• Non-regular fixed-point logic and games. In E. Grädel, J. Flum, and T. Wilke, editors, Logic and Automata: History and Perspectives, volume 2 of Texts in Logic and Games, pages 433–466. Amsterdam University Press, 2007.
  S. Kreutzer and M. Lange
  
• Temporal logics beyond regularity, 2007. Habilitation thesis, University of Munich, BRICS research report RS-07-13.
  M. Lange
  
• The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science, 3:1–33, 2007
  R. Axelsson, M. Lange, and R. Somla
  
• Three notes on the complexity of model checking fixpoint logic with chop. R.A.I.R.O. – Theoretical Informatics and Applications, 41:177–190, 2007.
  M. Lange
  
• Analyzing context-free grammars using an incremental SAT solver. In Proc. 35th Int. Coll. on Automata, Languages and Programming, ICALP’08, Part II, volume 5126 of LNCS, pages 410–422. Springer, 2008.
  R. Axelsson, K. Heljanko, and M. Lange
  
• A note on the relation between inflationary fixpoints and least fixpoints of higher-order. In Proc. of the 6th Workshop on Fixed Points in Computer Science, FICS’09, pages 54–60, 2009.
  S. Kreutzer and M. Lange