Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

On High-Quality Synthesis

verfasst von : Orna Kupferman

Erschienen in: Computer Science – Theory and Applications

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

In the synthesis problem, we are given a specification \(\psi \) over input and output signals, and we synthesize a system that realizes \(\psi \): with every sequence of input signals, the system associates a sequence of output signals so that the generated computation satisfies \(\psi \). The above classical formulation of the problem is Boolean. First, correctness is Boolean: a computation satisfies the specification \(\psi \) or does not satisfy it. Then, other important and interesting measures like the size of the synthesized system, its robustness, price, and so on, are ignored. The paper surveys recent efforts to address and formalize different aspects of quality of synthesized systems. We start with multi-valued specification formalisms, which refine the notion of correctness and enable the designer to specify quality, and continue to the quality measure of sensing: the detail in which the inputs should be read in order to generate a correct computation. The first part is based on the articles [1‐3]. The second part is based on [4, 5].

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Nächstes Kapitel Sensitivity Versus Certificate Complexity of Boolean Functions
Fußnoten
1
The observant reader may be concerned by our use of \(\max \) and \(\min \) where \(\sup \) and \(\inf \) are in order. In [3] we prove that there are only finitely many satisfaction values for a formula \(\varphi \), thus the semantics is well defined.
 
2
Observe that in our semantics the satisfaction value of future events tends to 0. One may think of scenarios where future events are discounted towards another value in [0, 1] (e.g., discounting towards \(\frac{1}{2}\) as ambivalence regarding the future).
 
3
We note that, alternatively, one could define the sensing level of states, with \({ slevel}(q)=\frac{{ scost}(q)}{|P|}\). Then, for all states q, we have that \({ slevel}(q) \in [0,1]\). All our results hold also for this definition, simply by dividing the sensing cost by |P|.
 
Literatur
1.
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)
2.
Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014)CrossRef
3.
Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. J. ACM (2016, to appear)
4.
Almagor, S., Kuperberg, D., Kupferman, O.: Regular sensing. In: Proceedings of the 34th Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 29, pp. 161–173. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2014)
5.
Almagor, S., Kuperberg, D., Kupferman, O.: The sensing cost of monitoring and synthesis. In: Proceedings of the 35th Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 35, pp. 380–393. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2015)
6.
Avni, G., Kupferman, O.: Synthesis from component libraries with costs. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 156–172. Springer, Heidelberg (2014)
7.
Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., Könighofer, B., Könighofer, R.: Synthesizing robust systems. Acta Inf. 51(3–4), 193–220 (2014)MathSciNetCrossRefMATH
8.
Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)CrossRef
9.
Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Environment assumptions for synthesis. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 147–161. Springer, Heidelberg (2008)CrossRef
10.
Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 380–395. Springer, Heidelberg (2010)CrossRef
11.
Church, A.: Logic, arithmetics, and automata. In: Proceedings of the International Congress of Mathematicians, 1962, pp. 23–35. Institut Mittag-Leffler (1963)
12.
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theor. Comput. Sci. 345(1), 139–170 (2005)MathSciNetCrossRefMATH
13.
Droste, M., Kuich, W., Vogler, H. (eds.): Handbook of Weighted Automata. Springer, Heidelberg (2009)MATH
14.
Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. Theor. Comput. Sci. 410(37), 3481–3494 (2009)MathSciNetCrossRefMATH
15.
Droste, M., Vogler, H.: Weighted automata and multi-valued logics over arbitrary bounded lattices. Theor. Comput. Sci. 418, 14–36 (2012)MathSciNetCrossRefMATH
16.
Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci. 220(3), 61–77 (2008)CrossRefMATH
17.
Fisman, D., Kupferman, O., Lustig, Y.: Rational synthesis. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 190–204. Springer, Heidelberg (2010)CrossRef
18.
Grinstead, C., Snell, J.L.: 11:Markov chains. In: Introduction to Probability. American Mathematical Society (1997)
19.
Kans, S.H.: Metrics and Models in Software Quality Engineering. Addison-Wesley Longman Publishing Co., Boston (2002)
20.
Krob, D.: The equality problem for rational series with multiplicities in the tropical semiring is undecidable. Int. J. Algebra Comput. 4(3), 405–425 (1994)MathSciNetCrossRefMATH
21.
Kupferman, O., Lustig, Y., Vardi, M.Y., Yannakakis, M.: Temporal synthesis for bounded systems and environments. In: Proceedings of the 28th Symposium on Theoretical Aspects of Computer Science, pp. 615–626 (2011)
22.
23.
Kwiatkowska, M.Z.: Quantitative verification: models techniques and tools. In: ESEC/SIGSOFT FSE, pp. 449–458 (2007)
24.
Mohri, M.: Finite-state transducers in language and speech processing. Comput. Linguist. 23(2), 269–311 (1997)MathSciNet
25.
Moon, S., Lee, K., Lee, D.: Fuzzy branching temporal logic. IEEE Trans. Syst. Man Cybern. Part B 34(2), 1045–1055 (2004)CrossRef
26.
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM Symposium on Principles of Programming Languages, pp. 179–190 (1989)
27.
Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)CrossRef
28.
Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects Comput. 6, 495–511 (1994)CrossRefMATH
29.
Spinellis, D.: Code Quality: The Open Source Perspective. Addison-Wesley Professional, Upper Saddle River (2006)
30.
Vardi, M.Y.: From verification to synthesis. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, p. 2. Springer, Heidelberg (2008)CrossRef
31.
Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of the 1st IEEE Symposium on Logic in Computer Science, pp. 332–344 (1986)
Metadaten
Titel
On High-Quality Synthesis
verfasst von
Orna Kupferman
Copyright-Jahr
2016
Buch
Computer Science – Theory and Applications

Print ISBN: 978-3-319-34170-5

Electronic ISBN: 978-3-319-34171-2

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-34171-2_1

Premium Partner

    Bildnachweise