University of Leicester
Browse

Synthesis of Reactive(1) designs

Download (525.2 kB)
journal contribution
posted on 2012-03-26, 15:50 authored by Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'Ar
We address the problem of automatically synthesizing digital designs from linear-time specifications. We consider various classes of specifications that can be synthesized with effort quadratic in the number of states of the reactive system, where we measure effort in symbolic steps. The synthesis algorithm is based on a novel type of game called General Reactivity of rank 1 (GR(1)), with a winning condition of the form (⃞⃟p1⋀...⋀⃞⃟pm)➙(⃞⃟q1⋀...⋀⃞⃟qn), where each pi and qi is a Boolean combination of atomic propositions. We show symbolic algorithms to solve this game, to build a winning strategy and several ways to optimize the winning strategy and to extract a system from it. We also show how to use GR(1) games to solve the synthesis of LTL specifications in many interesting cases. As empirical evidence to the generality and efficiency of our approach we include a significant case study. We describe the formal specifications and the synthesis process applied to a bus arbiter, which is a realistic industrial hardware specification of modest size.

History

Citation

Journal of Computer and System Sciences, 2012, 78 (3), pp. 911-938.

Author affiliation

/Organisation/COLLEGE OF SCIENCE AND ENGINEERING/Department of Computer Science

Version

  • AM (Accepted Manuscript)

Published in

Journal of Computer and System Sciences

Publisher

Elsevier

issn

0022-0000

eissn

1090-2724

Copyright date

2011

Available date

2012-03-26

Publisher version

http://www.sciencedirect.com/science/article/pii/S0022000011000869

Language

en

Usage metrics

    University of Leicester Publications

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC