Specification Decomposition for Synthesis from Libraries of LTL Assume/Guarantee Contracts
Antonio Iannopollo1,a, Stavros Tripakis1,2,c and Alberto Sangiovanni-Vincentelli1,b
1University of California, Berkeley Berkeley, USA
aantonio@berkeley.edu
balberto@berkeley.edu
2Aalto University, Aalto, Finland
cstavros@berkeley.edu
ABSTRACT
Contract-Based Design is a methodology that allows for compositional design of complex systems. Given a contract representing a specification, it is possible to formally satisfy it by composing a number of simpler contracts. When these simpler contracts are chosen from a library of existing solutions, we talk about synthesis from contract libraries. There are techniques to automate the synthesis process, but they are computationally intensive, especially for complex specifications. In this paper, we describe an efficient technique to partition a specification, i.e., an LTL-based Assume/Guarantee contract, in a number of simpler sub-specifications which can be satisfied independently. Once all these smaller problems are solved, it is possible to safely merge their solutions to satisfy the original specification. We show the effectiveness of our technique in an industrial case study.
