Enhancing Symbolic System Synthesis through ASPmT with Partial Assignment Evaluation

Kai Neubauer1,a, Philipp Wanko2,c, Torsten Schaub2,d and Christian Haubelt1,b
1University of Rostock, Applied Microelectronics and Computer Engineering, Germany.
akai.neubauer@uni-rostock.de
bchristian.haubelt@uni-rostock.de
2University of Potsdam, Knowledge Processing and Information Systems, Germany.
cwanko@cs.uni-potsdam.de
dtorsten@cs.uni-potsdam.de

ABSTRACT


The design of embedded systems is becoming continuously more complex such that efficient system-level design methods are becoming crucial. Recently, combined Answer Set Programming (ASP) and Quantifier Free Integer Difference Logic (QF 215 IDL) solving has been shown to be a promising approach in system synthesis. However, this approach still has several restrictions limiting its applicability. In the paper at hand, we propose a novel ASP modulo Theories (ASPmT) system synthesis approach, which (i) supports more sophisticated system models, (ii) tightly integrates the QF 215 IDL solving into the ASP solving, and (iii) makes use of partial assignment checking. As a result, more realistic systems are considered and an early exclusion of infeasible solutions improves the entire system synthesis.



Full Text (PDF)