Using Enhanced Logic Programming Semantics for Extending and Optimizing Synchronous System Design

  • The semantics of programming languages assign a meaning to the written program syntax. Currently, the meaning of synchronous programming languages, which are especially designed to develop programs for reactive and embedded systems, is based on a formal semantics definition similar to Fitting`s fixpoint semantics for logic programs. Nevertheless, it is possible to write a synchronous program code that does not evaluate to concrete values with the current semantics, which means those programs are currently seen to be not constructive. In the last decades, the theoretical knowledge and representation of semantics for logic programming has increased, but not all theoretical results and achievements have found their way to practice and application in system design. This thesis, in a first part, focuses on extensions to the semantics of synchronous programming languages to an evaluation similar to a well-founded semantics as defined in logic programming by van Gelder, Ross and Schlipf and to the stable model semantics as defined by Gelfond and Lifschitz. Particularly, this allows an evaluation for some of the currently not constructive programs where the semantics based on Fitting`s fixpoint fails. It is shown that the extension to well-founded semantics is a conservative extension of Fitting`s semantics, so that the meaning for programs which were already constructive does not change. Finally, it is considered how one can still generate circuits that implement the considered synchronous programs with the well-founded semantics. Again, this is a conservative approach that does not modify the circuits generated by the so-far used synthesis procedures. Answer set programming and the underlying stable model semantics describe problems by constraints and the related answer set solvers give all solutions to that problem as so-called answers. This allows the formulation of searching and planning problems as well as efficient solutions without having the need to develop special and possibly error-prone algorithms for every single application. The semantics of the synchronous programming language Quartz is also extended to the stable model semantics. For this extension, two alternatives are discussed: First of all, a direct extension similar to the extension to well-founded semantics is discussed. Second, a transformation of synchronous programs to the available answer set programming languages is given, as this allows to directly use answer set solvers for the synthesis and optimization of synchronous systems. The second part of the thesis contains further examples of the use of answer set programming in system design to emphasis their benefits for system design in general. The first example is hereby the generation of optimal/minimal interconnection-networks which allow non-blocking connections between n sources and n targets in parallel. As a second example, the stable model semantics is used to build a complete compiler chain, which transforms a given program to an optimal assembler code (called move code) for the new SCAD processor architecture which was developed at the University of Kaiserslautern. As a final part, the lessons learned from the two examples are shown by the means of some enhancement ideas for the synchronous programming language paradigm.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Marc DahlemORCiD
URN (permanent link):urn:nbn:de:hbz:386-kluedo-66332
Advisor:Klaus Schneider
Document Type:Doctoral Thesis
Language of publication:English
Publication Date:2021/10/30
Year of Publication:2021
Publishing Institute:Technische Universität Kaiserslautern
Granting Institute:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2021/08/17
Date of the Publication (Server):2021/11/02
Number of page:IX, 113
Faculties / Organisational entities:Fachbereich Informatik
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Creative Commons 4.0 - Namensnennung (CC BY 4.0)