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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 2/2013

01.04.2013

Weighted modal transition systems

verfasst von: Sebastian S. Bauer, Uli Fahrenberg, Line Juhl, Kim G. Larsen, Axel Legay, Claus Thrane

Erschienen in: Formal Methods in System Design | Ausgabe 2/2013

Einloggen

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

search-config
loading …

Abstract

Specification theories as a tool in model-driven development processes of component-based software systems have recently attracted a considerable attention. Current specification theories are however qualitative in nature, and therefore fragile in the sense that the inevitable approximation of systems by models, combined with the fundamental unpredictability of hardware platforms, makes it difficult to transfer conclusions about the behavior, based on models, to the actual system. Hence this approach is arguably unsuited for modern software systems. We propose here the first specification theory which allows to capture quantitative aspects during the refinement and implementation process, thus leveraging the problems of the qualitative setting.
Our proposed quantitative specification framework uses weighted modal transition systems as a formal model of specifications. These are labeled transition systems with the additional feature that they can model optional behavior which may or may not be implemented by the system. Satisfaction and refinement is lifted from the well-known qualitative to our quantitative setting, by introducing a notion of distances between weighted modal transition systems. We show that quantitative versions of parallel composition as well as quotient (the dual to parallel composition) inherit the properties from the Boolean setting.
Vorheriger Artikel An approximation algorithm for box abstraction of transition systems on real state spaces

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 "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

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
Literatur
1.
de Alfaro L, Faella M, Stoelinga M (2009) Linear and branching system metrics. IEEE Trans Softw Eng 35(2):258–273 CrossRef
2.
de Alfaro L, Henzinger T (2005) Interface-based design. In: Broy M, Grünbauer J, Harel D, Hoare T (eds) Engineering theories of software intensive systems. NATO science series II: mathematics, physics and chemistry, vol 195. Springer, Berlin, pp 83–104 CrossRef
3.
Aliprantis CD, Border KC (2007) Infinite dimensional analysis: a hitchhiker’s guide. Springer, Berlin
4.
Antonik A, Huth M, Larsen KG, Nyman U, Wąsowski A (2008) 20 years of modal and mixed specifications. Bull Eur Assoc Theor Comput Sci 95:94–129 MATH
5.
Basu A, Bensalem S, Bozga M, Caillaud B, Delahaye B, Legay A (2010) Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff J, Zucca E (eds) FMOODS/FORTE. Lecture notes in computer science, vol 6117. Springer, Berlin, pp 32–46
6.
Bauer SS, Fahrenberg U, Juhl L, Larsen KG, Legay A, Thrane C (2011) Quantitative refinement for weighted modal transition systems. In: Murlak F, Sankowski P (eds) MFCS. Lecture notes in computer science, vol 6907. Springer, Berlin, pp 60–71
7.
Bauer SS, Juhl L, Larsen KG, Legay A, Srba J (2012) Extending modal transition systems with structured labels. Math Struct Comput Sci 22(4):581–617 MathSciNetMATHCrossRef
8.
Beneš N, Černá I, Křetínský J (2011) Modal transition systems: composition and LTL model checking. In: Bultan T, Hsiung P-A (eds) ATVA. Lecture notes in computer science, vol 6996. Springer, Berlin, pp 228–242
9.
Beneš N, Křetínský J, Larsen KG, Srba J (2009) Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Leucker M, Morgan C (eds) ICTAC. Lecture notes in computer science, vol 5684. Springer, Berlin, pp 112–126
10.
Bonsangue MM, van Breugel F, Rutten JJMM (1998) Generalized metric spaces: completion, topology, and powerdomains via the Yoneda embedding. Theor Comput Sci 193(1–2):1–51 MATHCrossRef
11.
Černý P, Henzinger TA, Radhakrishna A (2012) Simulation distances. Theor Comput Sci 413(1):21–35 MATHCrossRef
12.
Chakrabarti A, de Alfaro L, Henzinger TA, Mang FYC (2002) Synchronous and bidirectional component interfaces. In: Brinksma E, Larsen KG (eds) CAV. Lecture notes in computer science, vol 2404. Springer, Berlin, pp 414–427
13.
Chatterjee K, de Alfaro L, Majumdar R, Raman V (2010) Algorithms for game metrics. Log Methods Comput Sci 6(3)
14.
Chatterjee K, Doyen L, Henzinger TA (2010) Expressiveness and closure properties for quantitative languages. Log Methods Comput Sci 6(3)
15.
16.
17.
David A, Larsen KG, Legay A, Nyman U, Wąsowski A (2010) Timed I/O automata: a complete specification theory for real-time systems. In: Johansson KH, Yi W (eds) HSCC. ACM, New York, pp 91–100 CrossRef
18.
de Alfaro L (2003) Quantitative verification and control via the mu-calculus. In: Amadio RM, Lugiez D (eds) CONCUR. Lecture notes in computer science, vol 2761. Springer, Berlin, pp 102–126
19.
de Alfaro L, Henzinger TA, Majumdar R (2003) Discounting the future in systems theory. In: Baeten JCM, Karel Lenstra J, Parrow J, Woeginger GJ (eds) ICALP. Lecture notes in computer science, vol 2719. Springer, Berlin, pp 1022–1037
20.
de Alfaro L, Majumdar R, Raman V, Stoelinga M (2008) Game refinement relations and metrics. Log Methods Comput Sci 4(3)
21.
Delahaye B (2010) Modular specification and compositional analysis of stochastic systems. PhD thesis, Université de Rennes 1
22.
Desharnais J, Gupta V, Jagadeesan R, Panangaden P (2004) Metrics for labelled Markov processes. Theor Comput Sci 318(3):323–354 MathSciNetMATHCrossRef
23.
24.
Droste M, Kuich W, Vogler H (2009) Handbook of weighted automata. EATCS monographs in theoretical computer science. Springer, Berlin MATHCrossRef
25.
26.
Fahrenberg U, Larsen KG, Thrane C (2010) A quantitative characterization of weighted Kripke structures in temporal logic. Comput Inform 29(6+):1311–1324 MathSciNet
27.
Fahrenberg U, Legay A, Thrane C (2011) The quantitative linear-time–branching-time spectrum. In: Chakraborty S, Kumar A (eds) FSTTCS. LIPIcs, vol 13. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Leibniz, pp 103–114
28.
Fahrenberg U, Thrane C, Larsen KG (2011) Distances for weighted transition systems: games and properties. In: Massink M, Norman G (eds) QAPL. Electronic proceedings in theoretical computer science, vol 57, pp 134–147
29.
Hall RJ (2000) Feature interactions in electronic mail. In: Calder M, Magill EH (eds) FIW. IOS Press, Amsterdam, pp 67–82
30.
31.
Larsen KG (1989) Modal specifications. In: Sifakis J (ed) Automatic verification methods for finite state systems. Lecture notes in computer science, vol 407. Springer, Berlin, pp 232–246 CrossRef
32.
Larsen KG, Fahrenberg U, Thrane C (2011) Metrics for weighted transition systems: axiomatization and complexity. Theor Comput Sci 412(28):3358–3369 MathSciNetMATHCrossRef
33.
Lawvere FW (1973) Metric spaces, generalized logic, and closed categories. Rend Semin Mat Fis Milano XLIII:135–166 MathSciNetCrossRef
34.
William Lawvere F (1986) Taking categories seriously. Rev Colomb Mat XX:147–178
35.
Lynch N, Tuttle MR (1989) An introduction to input/output automata. Quart - Cent Wiskd Inform 2(3)
36.
Majumdar R (2003) Symbolic algorithms for verification and control. PhD thesis, University of California, Berkeley
37.
Nyman U (2008) Modal transition systems as the basis for interface theories and product lines. PhD thesis, Aalborg University
38.
Raclet J-B (2008) Residual for component specifications. Electron Notes Theor Comput Sci 215:93–110 CrossRef
39.
Davide S (2009) On the origins of bisimulation and coinduction. ACM Trans Program Lang Syst 31(4)
40.
Sifakis J (2011) A vision for computer science—the system perspective. Cent. Eur. J. Comput. Sci. 1(1):108–116 CrossRef
41.
42.
Thrane C (2011) Quantitative models and analysis for reactive systems. PhD thesis, Aalborg University
43.
Thrane C, Fahrenberg U, Larsen KG (2010) Quantitative simulations of weighted transition systems. J Log Algebr Program 79(7):689–703 MathSciNetMATHCrossRef
44.
van Breugel F, (1994) Topological models in comparative semantics. PhD thesis, Vrije Universiteit, Amsterdam
45.
van Breugel F, (1996) A theory of metric labelled transition systems. Ann NY Acad Sci 806(1):69–87 CrossRef
46.
Zwick U, Paterson M (1995) The complexity of mean payoff games. In: Du D-Z, Li M (eds) COCOON. Lecture notes in computer science, vol 959. Springer, Berlin, pp 1–10
Metadaten
Titel
Weighted modal transition systems
verfasst von
Sebastian S. Bauer
Uli Fahrenberg
Line Juhl
Kim G. Larsen
Axel Legay
Claus Thrane
Publikationsdatum
01.04.2013
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 2/2013
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-012-0178-9

Premium Partner

    Bildnachweise