Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Acta Informatica
Published in: Acta Informatica 5/2014

01-08-2014 | Original Article

General quantitative specification theories with modal transition systems

Authors: Uli Fahrenberg, Axel Legay

Published in: Acta Informatica | Issue 5/2014

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

This paper proposes a new theory of quantitative specifications. It generalizes the notions of step-wise refinement and compositional design operations from the Boolean to an arbitrary quantitative setting. Using a great number of examples, it is shown that this general approach permits to unify many interesting quantitative approaches to system design.
next article Forward and backward application of symbolic tree transducers

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now
Literature
1.
Aliprantis, C.D., Border, K.C.: Infinite Dimensional Analysis: A Hitchhiker’s Guide. Springer, Berlin (2007)
2.
3.
Bauer, S.S., David, A., Hennicker, R., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE, volume 7212 of Lecture Notes in Computer Science, pp. 43–58. Springer, Berlin (2012)
4.
Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.: Quantitative refinement for weighted modal transition systems. In: Murlak, F., Sankowski, P. (eds.) MFCS, volume 6907 of Lecture Notes in Computer Science, pp. 60–71. Springer, Berlin (2011)
5.
Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, Claus: Weighted modal transition systems. Form. Methods Syst. Des. 42(2), 193–220 (2013)CrossRefMATH
6.
Bauer, S.S., Fahrenberg, U., Legay, A., Thrane, C.: General quantitative specification theories with modalities. In: Hirsch, E.A., Karhumäki, J., Lepistö, A., Prilutskii, M. (eds.) CSR, volume 7353 of Lecture Notes in Computer Science, pp. 18–30. Springer, Berlin (2012)
7.
Bauer, S.S., Juhl, L., Larsen, K.G., Legay, A., Srba, J.: Extending modal transition systems with structured labels. Math. Struct. Comput. Sci. 22(4), 581–617 (2012)CrossRefMATHMathSciNet
8.
Bauer, S.S., Juhl, L., Larsen, K.G., Srba, J., Legay, A.: A logic for accumulated-weight reasoning on multiweighted modal automata. In: Margaria, T., Qiu, Z., Yang, H. (eds.) TASE, pp. 77–84. IEEE (2012)
9.
Beneš, N., Černá, I., Křetínský, J.: Modal transition systems: composition and LTL model checking. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA, volume 6996 of Lecture Notes in Computer Science, pp. 228–242. Springer, Berlin (2011)
10.
Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bjørner, N., Voronkov, A. (eds.) LPAR, volume 7180 of Lecture Notes in Computer Science, pp. 122–137. Springer, Berlin (2012)
11.
Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: On determinism in modal transition systems. Theor. Comput. Sci. 410(41), 4026–4043 (2009)CrossRefMATH
12.
Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: A compositional approach on modal specifications for timed systems. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM, volume 5885 of Lecture Notes in Computer Science, pp. 679–697. Springer, Berlin (2009)
13.
Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.-B.: Modal event-clock specifications for timed component-based design. Sci. Comput. Program. 77(12), 1212–1234 (2012)CrossRefMATH
14.
Bertrand, N., Pinchinat, S., Raclet, J.-B.: Refinement and consistency of timed modal specifications. In: Dediu, A.H., Ionescu, A.-M., Martín-Vide, C. (eds.) LATA, volume 5457 of Lecture Notes in Computer Science, pp. 152–163. Springer, Berlin (2009)
15.
Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Commun. ACM 54(9), 78–87 (2011)CrossRef
16.
Bouyer, P., Larsen, K.G., Markey, N., Sankur, O., Thrane, C.R.: Timed automata can always be made implementable. In: Katoen, J.-P., König, B. (eds.) CONCUR, volume 6901 of Lecture Notes in Computer Science, pp. 76–91. Springer, Berlin (2011)
17.
Černý, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. In: Gastin, P., Laroussinie, F. (eds.) CONCUR, volume 6269 of Lecture Notes in Computer Science, pp. 253–268. Springer, Berlin (2010)
18.
Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4), 1–23 (2010)
19.
David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: Timed I/O automata: a complete specification theory for real-time systems. In: Johansson, K.H., Yi, W. (eds.) HSCC, pp. 91–100. ACM, New York (2010)CrossRef
20.
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258–273 (2009)CrossRef
21.
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP, volume 2719 of Lecture Notes in Computer Science, pp. 1022–1037. Springer, Berlin (2003)
22.
Desharnais, J., Laviolette, F., Tracol, M.: Approximate analysis of probabilistic processes. In: QEST, pp. 264–273. IEEE Computer Society (2008)
23.
Doyen, L., Henzinger, T.A., Legay, A., Ničković, D.: Robustness of sequential circuits. In: Gomes, L., Khomenko, V., Fernandes, J. (eds.) ACSD, pp. 77–84. IEEE Computer Society, Washington (2010)
24.
25.
Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy games in multiweighted automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC, volume 6916 of Lecture Notes in Computer Science, pp. 95–115. Springer, Berlin (2011)
26.
Fahrenberg, U., Legay, A.: A robust specification theory for modal event-clock automata. In: Bauer, S.S., Raclet, J.-B. (eds.) FIT, volume 87 of Electronic Proceedings in Theoretical Computer Science, pp. 5–16 (2012)
27.
Fahrenberg, U., Legay, A., Thrane, C.: The quantitative linear-time-branching-time spectrum. In: Chakraborty, S., Kumar, A. (eds.) FSTTCS, volume 13 of Leibniz International Proceedings in Informatics, pp. 103–114. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2011)
28.
Fahrenberg, U., Legay, A., Wąsowski, A.: Make a difference! (Semantically). In: Whittle, J., Clark, T., Kühne, T. (eds.) MoDELS, volume 6981 of Lecture Notes in Computer Science, pp. 490–500. Springer, Berlin (2011)
29.
Fahrenberg, U., Thrane, C., Larsen, K.G.: Distances for weighted transition systems: games and properties. In: Massink, M., Norman, G. (eds.) QAPL, volume 57 of Electronic Proceedings in Theoretical Computer Science, pp. 134–147 (2011)
30.
Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR, volume 2154 of Lecture Notes in Computer Science, pp. 426–440. Springer, Berlin (2001)
31.
Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS, volume 5051 of Lecture Notes in Computer Science, pp. 113–131. Springer, Berlin (2008)
32.
Grumberg, O., Lange, M., Leucker, M., Shoham, S.: Don’t know in the \(\mu \)-calculus. In: Cousot, R. (ed.) VMCAI, volume 3385 of Lecture Notes in Computer Science, pp. 233–249. Springer, Berlin (2005)
33.
Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART, volume 1201 of Lecture Notes in Computer Science, pp. 331–345. Springer, Berlin (1997)
34.
Henzinger, T.A., Majumdar, R., Prabhu, V.S.: Quantifying similarities between timed systems. In: Pettersson, P., Yi, W. (eds.) FORMATS, volume 3829 of Lecture Notes in Computer Science, pp. 226–241. Springer, Berlin (2005)
35.
36.
Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems, volume 407 of Lecture Notes in Computer Science, pp. 232–246. Springer, Berlin (1989)
37.
Larsen, K.G., Fahrenberg, U., Thrane, C.: Metrics for weighted transition systems: axiomatization and complexity. Theor. Comput. Sci. 412(28), 3358–3369 (2011)CrossRefMATHMathSciNet
38.
Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)MATH
39.
Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)MATH
40.
Nyman, U.: Modal Transition Systems as the Basis for Interface Theories and Product Lines. PhD thesis, Aalborg University, September (2008)
41.
Park, D.M.R.: Concurrency and automata on infinite sequences. In: Theoretical Computer Science, volume 104 of Lecture Notes in Computer Science, pp. 167–183. Springer, Berlin (1981)
42.
Rasmussen, J.I., Larsen, K.G., Subramani, K.: On using priced timed automata to achieve optimal scheduling. Form. Methods Syst. Des. 29(1), 97–114 (2006)CrossRefMATH
43.
Swaminathan, M., Fränzle, M.: A symbolic decision procedure for robust safety of timed systems. In: TIME, p. 192. IEEE Computer Society, Washington (2007)
44.
Swaminathan, M., Fränzle, M., Katoen, J.-P.: The surprising robustness of (closed) timed automata against clock-drift. In: Ausiello, G., Karhumäki, J., Mauri, G., Ong, C.-H.L. (eds.) IFIP TCS, volume 273 of IFIP, pp. 537–553. Springer, Berlin (2008)
45.
46.
Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative simulations of weighted transition systems. J. Log. Algebr. Program. 79(7), 689–703 (2010)CrossRefMATHMathSciNet
47.
van Breugel, F.: A theory of metric labelled transition systems. Ann. NY Acad. Sci. 806(1), 69–87 (1996)CrossRef
48.
van Breugel, F.: A behavioural pseudometric for metric labelled transition systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR, volume 3653 of Lecture Notes in Computer Science, pp. 141–155. Springer, Berlin (2005)
49.
Winskel, G., Nielsen, M.: Models for concurrency. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 4, pp. 1–148. Clarendon Press, Oxford (1995)
50.
Zwick, U., Paterson, M.: The complexity of mean payoff games. In: Computing and Combinatorics, volume 959 of Lecture Notes in Computer Science, pp. 1–10. Springer, Berlin (1995)
Metadata
Title
General quantitative specification theories with modal transition systems
Authors
Uli Fahrenberg
Axel Legay
Publication date
01-08-2014
Publisher
Springer Berlin Heidelberg
Published in
Acta Informatica / Issue 5/2014
Print ISSN: 0001-5903
Electronic ISSN: 1432-0525
DOI
https://doi.org/10.1007/s00236-014-0196-8

Premium Partner

    Image Credits