Component-based synthesis using combinatory logic, intersection types and predicates

Abstract

In dieser Arbeit wird eine neue Version des Combinatory Logic Synthesizer ((CL)S) vorgestellt, der Combinatory Logic Synthesizer with Predicates (CLSP) genannt wird. Dieses neue Framework verwendet Inhabitation in der kürzlich entwickelten Finite Combinatory Logic with Predicates (FCLP) anstelle der Finite Combinatory Logic (FCL), die in früheren Iterationen verwendet wird. FCLP bietet neue Spezifikationsmöglichkeiten durch die Hinzufügung von parametrisierten Typen, die es erlauben, von einer endlichen Menge von Literalen abzuhängen und durch Prädikate eingeschränkt zu werden. Der Fokus von CLSP unterscheidet sich von früheren Iterationen von (CL)S darin, dass er mit Schwerpunkt auf Ausführungsgeschwindigkeit und Benutzerfreundlichkeit entwickelt wurde, anstatt auf beweisbare Korrektheit. Sowohl die theoretischen Grundlagen des Frameworks als auch die Implementierung in Python werden diskutiert. Eine Evaluation des Frameworks in Form von Benchmarks wird präsentiert, die verschiedene Modellierungstechniken des neuen Frameworks miteinander vergleicht, sowie die Synthesegeschwindigkeit von CLSP mit früheren Iterationen von (CL)S. Letzteres zeigt eine Verbesserung der Laufzeit von bis zu 100-fach, verglichen mit der schnellsten (CL)S Version, in bestimmten Benchmarks. Weiterhin wird eine prototypische parallele Implementierung des Inhabitationsalgorithmus vorgestellt, der eine beinahe lineare Beschleunigung in der Anzahl der verwendeten CPU-Kerne zeigt. Abschließend werden zwei Anwendungen des Frameworks diskutiert, eins, zum Finden von Strategien in einem Fragment von LTL, und eins, im Kontext von Simulationsmodellen in Materialflusssystemen. Dies zeigt, wie das Framework sowohl in theoretischen und praktischen Anwendungen genutzt werden kann.