nach oben

Acta Informatica

Erschienen in:

01.04.2015 | Original Article

Refinement checking on parametric modal transition systems

verfasst von: Nikola Beneš, Jan Křetínský, Kim G. Larsen, Mikael H. Møller, Salomon Sickert, Jiří Srba

Erschienen in: Acta Informatica | Ausgabe 2-3/2015

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Modal transition systems (MTS) is a well-studied specification formalism of reactive systems supporting a step-wise refinement methodology. Despite its many advantages, the formalism as well as its currently known extensions are incapable of expressing some practically needed aspects in the refinement process like exclusive, conditional and persistent choices. We introduce a new model called parametric modal transition systems (PMTS) together with a general modal refinement notion that overcomes many of the limitations. We investigate the computational complexity of modal and thorough refinement checking on PMTS and its subclasses and provide a direct encoding of the modal refinement problem into quantified Boolean formulae, allowing us to employ state-of-the-art QBF solvers for modal refinement checking. The experiments we report on show that the feasibility of refinement checking is more influenced by the degree of nondeterminism rather than by the syntactic restrictions on the types of formulae allowed in the description of the PMTS.

Vorheriger Artikel Moving from interface theories to assembly theories

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

In the transition systems with obligations only positive Boolean formulae are allowed.

http://fmv.jku.at/quantor/.

Aceto, L., Fábregas, I., de Frutos-Escrig, D., Ingólfsdóttir, A., Palomino, M.: Graphical representation of covariant-contravariant modal formulae. In: EXPRESS, pp. 1–15 (2011)

Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: CONCUR, pp. 163–178 (1998)

Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94–129 (2008)MATHMathSciNet

Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: Complexity of decision problems for mixed and modal specifications. In: Proceedings of the 11th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’08), LNCS, vol. 4962, pp. 112–126 (2008)

Balcazar, J.L., Gabarró, J., Santha, M.: Deciding bisimilarity is P-complete. Form. Asp. Comput. 4(6 A), 638–648 (1992)

Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.R.: Quantitative refinement for weighted modal transition systems. In: MFCS, LNCS, vol. 6907, pp. 60–71. Springer, Berlin (2011)

Beneš, N., Černá, I., Křetínský, J.: Disjunctive Modal Transition Systems and Generalized LTL Model Checking. Technical report FIMU-RS-2010-12, Faculty of Informatics, Masaryk University, Brno (2010)

Beneš, N., Delahaye, B., Fahrenberg, U., Křetínský, J., Legay, A.: Hennessy–Milner logic with greatest fixed points as a complete behavioural specification theory. In: D’Argenio, P.R., Melgratti, H.C. (eds.) CONCUR, Lecture Notes in Computer Science, vol. 8052, pp. 76–90. Springer, Berlin (2013)

Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric Modal Transition Systems. Technical report FIMU-RS-2011-03, Faculty of Informatics, Masaryk University, Brno (2011)

10.

Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218, 54–68 (2012)CrossRefMATH

11.

Beneš, N., Křetínský, J.: Process algebra for modal transition systemses. In: Matyska, L., Kozubek, M., Vojnar, T., Zemcík, P., Antos, D. (eds.) MEMICS, OASICS, vol. 16, pp. 9–18. Schloss Dagstuh—Leibniz-Zentrum fuer Informatik, Germany (2010)

12.

Beneš, N., Křetínský, J., Larsen, K., Srba, J.: EXPTIME-completeness of thorough refinement on modal transition systems. Inf. Comput. 218, 54–68 (2012)CrossRefMATH

13.

Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: ATVA, pp. 275–289 (2011)

14.

Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: LPAR, pp. 122–137 (2012)

15.

Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Proceedings of the Theoretical Aspects of Computing—ICTAC 2009, 6th International Colloquium, LNCS, vol. 5684. Springer, Berlin (2009)

16.

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

17.

Beneš, N., Černá, I., Křetínský, J.: Modal transition systems: Composition and LTL model checking. In: ATVA, pp. 228–242 (2011)

18.

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). doi:10.1016/j.scico.2011.01.007 CrossRefMATH

19.

Boudol, G., Larsen, K.G.: Graphical versus logical specifications. In: CAAP, pp. 57–71 (1990)

20.

Boudol, G., Larsen, K.G.: Graphical versus logical specifications. Theor. Comput. Sci. 106(1), 3–20 (1992)CrossRefMATHMathSciNet

21.

Caillaud, B., Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: Compositional design methodology with constraint markov chains. In: QEST, pp. 123–132 (2010)

22.

Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don’t Know for multi-valued systems. In: ATVA, pp. 289–305 (2009)

23.

Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification—theory and tools. In: CAV, pp. 253–267 (1993)

24.

de Alfaro, L., Henzinger, T.A.: Interface automata. In: ESEC/SIGSOFT FSE, pp. 109–120 (2001)

25.

Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst. 19(2), 253–291 (1997)CrossRef

26.

Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS, pp. 335–344 (2004)

27.

David, A., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: ECDAR: An environment for compositional design and analysis of real time systems. In: ATVA, pp. 365–370 (2010)

28.

Fecher, H., Schmidt, H.: Comparing disjunctive modal transition systems with an one-selecting variant. J. Logic Algebr. Program. 77(1–2), 20–39 (2008)CrossRefMATHMathSciNet

29.

Fecher, H., Steffen, M.: Characteristic mu-calculus formulas for underspecified transition systems. ENTCS 128(2), 103–116 (2005)

30.

Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Proceedings of the CONCUR’01, LNCS, vol. 2154, pp. 426–440. Springer, Berlin (2001)

31.

Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional may-must program analysis: unleashing the power of alternation. In: POPL, pp. 43–56 (2010)

32.

Gruler, A., Leucker, M., Scheidemann, K.D.: Modeling and model checking software product lines. In: Barthe, G., de Boer, F.S. (eds.) FMOODS, Lecture Notes in Computer Science, vol. 5051, pp. 113–131. Springer, Berlin (2008)

33.

Huth, M., Jagadeesan, R., Schmidt, D.A.: Modal transition systems: a foundation for three-valued program analysis. In: Proceedings of the ESOP’01, LNCS, vol. 2028, pp. 155–169. Springer, Berlin (2001)

34.

Jacobs, B., Poll, E.: A logic for the java modeling language JML. In: FASE, pp. 284–299 (2001)

35.

Juhl, L., Larsen, K.G., Srba, J.: Modal transition systems with weight intervals. J. Log. Algebr. Program. 81(4), 408–421 (2012)CrossRefMATHMathSciNet

36.

Křetínský, J., Sickert, S.: MoTraS: A tool for modal transition systems and their extensions. In: Hung, D.V., Ogawa, M. (eds.) ATVA, Lecture Notes in Computer Science, vol. 8172, pp. 487–491. Springer, Berlin (2013). Tool accessible at https://www7.in.tum.de/kretinsk/motras.html

37.

Křetínský, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC, Lecture Notes in Computer Science, vol. 8049, pp. 213–230. Springer, Berlin (2013)

38.

Křetínský, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. CoRR abs/1304.5278 (2013)

39.

Larsen, K.G., Nyman, U., Wasowski, A.: Modal I/O automata for interface and product line theories. In: ESOP, pp. 64–79 (2007)

40.

Larsen, K.G., Nyman, U., Wasowski, A.: On modal refinement and consistency. In: Proceedings of the CONCUR’07, LNCS, vol. 4703, pp. 105–119. Springer, Berlin (2007)

41.

Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)

42.

Larsen, K.G., Xinxin, L.: Equation solving using modal transition systems. In: LICS, pp. 108–117. IEEE Computer Society (1990)

43.

Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)CrossRef

44.

Lüttgen, G., Vogler, W.: Modal interface automata. Log. Methods Comput. Sci. 9(3) (2013). doi:10.2168/LMCS-9(3:4)2013

45.

Lynch, N.: I/O automata: A model for discrete event systems. In: 22nd Annual Conference on Information Sciences and Systems, pp. 29–38. Princeton University, Princeton (1988)

46.

Namjoshi, K.S.: Abstraction for branching time properties. In: CAV, pp. 288–300 (2003)

47.

Nanz, S., Nielson, F., Nielson, H.R.: Modal abstractions of concurrent behaviour. In: Proceeding of the SAS’08, LNCS, vol. 5079, pp. 159–173. Springer, Berlin (2008)

48.

Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)MATH

49.

Raclet, J.B.: Quotient de Spécifications pour la Réutilisation de Composants. Ph.D. thesis, Université de Rennes I (2007); (in French)

50.

Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fundamenta Informaticae 108(1–2), 119–149 (2011)

51.

Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Passerone, R.: Why are modalities good for interface theories? In: ACSD, pp. 119–127. IEEE (2009)

52.

Sawa, Z., Jančar, P.: Behavioural equivalences on finite-state systems are PTIME-hard. Comput. Inf. 24(5), 513–528 (2005)MATH

53.

Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Proceedings of the FSE’04, pp. 43–52. ACM (2004)

Titel: Refinement checking on parametric modal transition systems
verfasst von: Nikola Beneš
Jan Křetínský
Kim G. Larsen
Mikael H. Møller
Salomon Sickert
Jiří Srba
Publikationsdatum: 01.04.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 2-3/2015
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-015-0215-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 2-3/2015

Modal algebra and Petri nets

Observable liveness of Petri nets

Special issue on “Comprehending asynchrony in specification and analysis” dedicated to Walter Vogler on the occasion of his 60th birthday

Moving from interface theories to assembly theories

State space axioms for T-systems

CCS: It’s not fair!