Synthesis from Component Libraries with Costs

  • Guy Avni
  • Orna Kupferman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8704)


Synthesis is the automated construction of a system from its specification. In real life, hardware and software systems are rarely constructed from scratch. Rather, a system is typically constructed from a library of components. Lustig and Vardi formalized this intuition and studied LTL synthesis from component libraries. In real life, designers seek optimal systems. In this paper we add optimality considerations to the setting. We distinguish between quality considerations (for example, size – the smaller a system is, the better it is), and pricing (for example, the payment to the company who manufactured the component). We study the problem of designing systems with minimal quality-cost and price. A key point is that while the quality cost is individual – the choices of a designer are independent of choices made by other designers that use the same library, pricing gives rise to a resource-allocation game – designers that use the same component share its price, with the share being proportional to the number of uses (a component can be used several times in a design). We study both closed and open settings, and in both we solve the problem of finding an optimal design. In a setting with multiple designers, we also study the game-theoretic problems of the induced resource-allocation game.


Nash Equilibrium Correct Design Construction Cost Winning Strategy Full Version 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable concurrent program specifications. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)CrossRefGoogle Scholar
  2. 2.
    Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 15–27. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  3. 3.
    Alonso, G., Casati, F., Kuno, H.A., Machiraju, V.: Web Services - Concepts, Architectures and Applications. In: Data-Centric Systems and Applications. Springer (2004)Google Scholar
  4. 4.
    Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  5. 5.
    Avni, G., Kupferman, O.: When does abstraction help? IPL 113, 901–905 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  6. 6.
    Avni, G., Kupferman, O., Tamir, T.: Congestion and cost-sharing games with multisets of resources (submitted, 2014)Google Scholar
  7. 7.
    Avni, G., Kupferman, O., Tamir, T.: Network-formation games with regular objectives. In: Muscholl, A. (ed.) FOSSACS 2014. LNCS, vol. 8412, pp. 119–133. Springer, Heidelberg (2014)Google Scholar
  8. 8.
    Berwanger, D., Doyen, L.: On the power of imperfect information. In: Proc. 28th TST& TCS, pp. 73–82 (2008)Google Scholar
  9. 9.
    Bohy, A., Bruyère, V., Filiot, E., Raskin, J.-F.: Synthesis from LTL specifications with mean-payoff objectives. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 169–184. Springer, Heidelberg (2013)Google Scholar
  10. 10.
    Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: Proc. 26th LICS, pp. 43–52 (2011)Google Scholar
  11. 11.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. TCS 345(1), 139–170 (2005)CrossRefzbMATHGoogle Scholar
  12. 12.
    de Alfaro, L., Henzinger, T.A.: Interface theories for component-based design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  13. 13.
    Doyen, L., Henzinger, T.A., Jobstmann, B., Petrov, T.: Interface theories with component reuse. In: Proc. 8th EMSOFT, pp. 79–88 (2008)Google Scholar
  14. 14.
    Elgaard, J., Klarlund, N., Möller, A.: Mona 1.x: New techniques for WS1S and WS2S. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 516–520. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  15. 15.
    Fabrikant, A., Papadimitriou, C., Talwar, K.: The complexity of pure nash equilibria. In: Proc. 36th STOC, pp. 604–612 (2004)Google Scholar
  16. 16.
    Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. ENTCS 220(3), 61–77 (2008)Google Scholar
  17. 17.
    Filiot, E., Jin, N., Raskin, J.-F.: Antichains and compositional algorithms for LTL synthesis. FMSD 39(3), 261–296 (2011)zbMATHGoogle Scholar
  18. 18.
    Gößler, G., Sifakis, J.: Composition for component-based modeling. Sci. Comput. Program. 55(1-3), 161–183 (2005)CrossRefzbMATHGoogle Scholar
  19. 19.
    Jurdziński, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Ko, K.-I., Lin, C.-L.: On the complexity of min-max optimization problems and their approximation. In: Minimax and Applications. Nonconvex Optimization and Its Applications, vol. 4, pp. 219–239. Springer (1995)Google Scholar
  21. 21.
    Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31–44. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  22. 22.
    Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: Proc. 46th FOCS, pp. 531–540 (2005)Google Scholar
  23. 23.
    Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. STTT 15, 603–618 (2013)CrossRefGoogle Scholar
  24. 24.
    Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th POPL, pp. 179–190 (1989)Google Scholar
  25. 25.
    Raskin, J.-F., Chatterjee, K., Doyen, L., Henzinger, T.: Algorithms for ω-regular games with imperfect information. LMCS 3(3) (2007)Google Scholar
  26. 26.
    Roughgarden, T., Tardos, E.: How bad is selfish routing? JACM 49(2), 236–259 (2002)CrossRefMathSciNetGoogle Scholar
  27. 27.
    Safra, S.: On the complexity of ω-automata. In: Proc. 29th FOCS, pp. 319–327 (1988)Google Scholar
  28. 28.
    Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logic. JACM 32, 733–749 (1985)CrossRefzbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Guy Avni
    • 1
  • Orna Kupferman
    • 1
  1. 1.School of Computer Science and EngineeringThe Hebrew UniversityIsrael

Personalised recommendations