Iterative Circuit Repair Against Formal Specifications

Cosler, Matthias and Schmitt, Frederik and Hahn, Christopher and Finkbeiner, Bernd
(2023) Iterative Circuit Repair Against Formal Specifications.
In: Eleventh International Conference on Learning Representations.
Conference: ICLR International Conference on Learning Representations

[img] Text
Iterative Circuit Repair Against Formal Specifications - Final Version.pdf
Download (571kB)

Abstract

We present a deep learning approach for repairing sequential circuits against formal specifications given in linear-time temporal logic (LTL). Given a defective circuit and its formal specification, we train Transformer models to output circuits that satisfy the corresponding specification. We propose a separated hierarchical Transformer for multimodal representation learning of the formal specification and the circuit. We introduce a data generation algorithm that enables generalization to more complex specifications and out-of-distribution datasets. In addition, our proposed repair mechanism significantly improves the automated synthesis of circuits from LTL specifications with Transformers. It improves the state-of-the-art by 6.8 percentage points on held-out instances and 11.8 percentage points on an out-of-distribution dataset from the annual reactive synthesis competition.

Item Type: Conference or Workshop Item (A Paper) (Poster)
Divisions: Bernd Finkbeiner (Reactive Systems Group, RSG)
Conference: ICLR International Conference on Learning Representations
Depositing User: Frederik Schmitt
Date Deposited: 25 Jul 2023 14:06
Last Modified: 25 Jul 2023 14:06
Primary Research Area: NRA2: Reliable Security Guarantees
URI: https://publications.cispa.saarland/id/eprint/3992

Actions

Actions (login required)

View Item View Item
CISPA is powered by EPrints 3 which is developed by the School of Electronics and Computer Science at the University of Southampton. More information and software credits.