[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

30 Years of Modal Transition Systems: Survey of Extensions and Analysis

  • Chapter
  • First Online:
Models, Algorithms, Logics and Tools

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10460))

Abstract

We survey the specification formalism of modal transition systems (MTS). We discuss various extensions of MTS, their relationships and modelling capabilities. The extensions include more involved modalities, quantitative aspects, or infinite state spaces. Further, we discuss problems arising in verification and analysis of these systems. We cover refinement checking, model checking and synthesis, standard logical and structural operations as used in specification theories as well as the respective tool support.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

eBook
GBP 12.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The notation introduced in [BKLS09b] is adopted from semantics.

  2. 2.

    In the context of MTS, [Ben12] elaborates on the differences of the two.

References

  1. Aceto, L., Fábregas, I., Frutos Escrig, D., Ingólfsdóttir, A., Palomino, M.: Relating modal refinements, covariant-contravariant simulations and partial bisimulations. In: Arbab, F., Sirjani, M. (eds.) FSEN 2011. LNCS, vol. 7141, pp. 268–283. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29320-7_18

    Chapter  Google Scholar 

  2. Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998). doi:10.1007/BFb0055622

    Chapter  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  4. Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wąsowski, A.: Complexity of decision problems for mixed and modal specifications. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 112–126. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78499-9_9

    Chapter  Google Scholar 

  5. Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: EXPTIME-complete decision problems for modal and mixed specifications. Electron. Notes Theor. Comput. Sci. 242(1), 19–33 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: An inductive approach for modal transition system refinement. In: Gallagher, J.P., Gelfond, M. (eds) ICLP (Technical Communications). LIPIcs, vol. 11, pp. 106–116. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)

    Google Scholar 

  7. Bauer, S.S:. Modal specification theories for component-based design. Ph.D. thesis, Ludwig Maximilians University Munich (2012)

    Google Scholar 

  8. 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)

    Google Scholar 

  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 2011. LNCS, vol. 6996, pp. 228–242. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_17

    Chapter  Google Scholar 

  10. Brunet, G., Chechik, M., Uchitel, S.: Properties of behavioural model merging. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 98–114. Springer, Heidelberg (2006). doi:10.1007/11813040_8

    Chapter  Google Scholar 

  11. Ben-David, S., Chechik, M., Uchitel, S.: Observational refinement and merge for disjunctive MTSs. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 287–303. Springer, Cham (2016). doi:10.1007/978-3-319-46520-3_19

    Chapter  Google Scholar 

  12. Ben-David, S., Chechik, M., Uchitel, S.: Merging partial behaviour models with different vocabularies. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 91–105. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40184-8_8

    Chapter  Google Scholar 

  13. 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. (eds.) CONCUR 2013. LNCS, vol. 8052, pp. 76–90. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40184-8_7

    Chapter  Google Scholar 

  14. Bauer, S.S., David, A., Hennicker, R., Guldstrand Larsen, K., Legay, A., Nyman, U., Wąsowski, A.: Moving from specifications to contracts in component-based design. In: Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43–58. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28872-2_3

    Chapter  Google Scholar 

  15. Beneš, N., Daca, P., Henzinger, T.A., Křetínský, J., Nickovic, D.: Complete composition operators for IOCO-testing theory. In: Kruchten, P., Becker, S., Schneider, J.-G. (eds.) Proceedings of the 18th International ACM SIGSOFT Symposium on Component-Based Software Engineering, CBSE 2015, Montreal, QC, Canada, 4–8 May 2015, pp. 101–110. ACM (2015)

    Google Scholar 

  16. Benveniste, A.: Multiple viewpoint contracts and residuation. In: 2nd International Workshop on Foundations of Interface Technologies (FIT) (2008)

    Google Scholar 

  17. Beneš, N.: Disjunctive modal transition systems. Ph.D. thesis, Masaryk University (2012)

    Google Scholar 

  18. 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 2011. LNCS, vol. 6907, pp. 60–71. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22993-0_9

    Chapter  Google Scholar 

  19. Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.R.: Weighted modal transition systems. Formal Methods Syst. Des. 42(2), 193–220 (2013)

    Article  MATH  Google Scholar 

  20. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol. 5215, pp. 33–47. Springer, Heidelberg (2008). doi:10.1007/978-3-540-85778-5_4

    Chapter  Google Scholar 

  21. 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 2012. LNCS, vol. 7353, pp. 18–30. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30642-6_3

    Chapter  Google Scholar 

  22. Bujtor, F., Fendrich, S., Lüttgen, G., Vogler, W.: Nondeterministic modal interfaces. Theor. Comput. Sci. 642, 24–53 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  23. Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999). doi:10.1007/3-540-48683-6_25

    Chapter  Google Scholar 

  24. Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000). doi:10.1007/3-540-44618-4_14

    Chapter  Google Scholar 

  25. Balcázar, J.L., Gabarró, J., Santha, M.: Deciding bisimilarity is p-complete. Formal Asp. Comput. 4(6A), 638–648 (1992)

    Article  MATH  Google Scholar 

  26. Bultan, T., Hsiung, P.-A. (eds.): ATVA 2011. LNCS, vol. 6996. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1

    MATH  Google Scholar 

  27. Bauer, S.S., Hennicker, R., Bidoit, M.: A modal interface theory with data constraints. In: Davies, J., Silva, L., Simao, A. (eds.) SBMF 2010. LNCS, vol. 6527, pp. 80–95. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19829-8_6

    Chapter  Google Scholar 

  28. Bauer, B.B., Hennicker, R., Janisch, S.: Interface theories for (a)synchronously communicating modal I/O-transition systems. In: Legay, A., Caillaud, B. (eds.) FIT. EPTCS, vol. 46, pp. 1–8 (2010)

    Google Scholar 

  29. Bauer, S.S., Hennicker, R., Wirsing, M.: Building a modal interface theory for concurrency and data. In: Mossakowski, T., Kreowski, H.-J. (eds.) WADT 2010. LNCS, vol. 7137, pp. 1–12. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28412-0_1

    Chapter  Google Scholar 

  30. 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)

    Article  MathSciNet  MATH  Google Scholar 

  31. 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)

    Google Scholar 

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

    Google Scholar 

  33. Beneš, N., Křetínský, J.: Modal process rewrite systems. In: Roychoudhury, A., D’Souza, M. (eds.) [RD12], pp. 120–135

    Google Scholar 

  34. Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Srba, J.: Parametric modal transition systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 275–289. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_20

    Chapter  Google Scholar 

  35. Beneš, N., Křetínský, J., Guldstrand Larsen, K., Møller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 122–137. Springer, Heidelberg (2012). doi:10.1007/978-3-642-28717-6_12

    Chapter  Google Scholar 

  36. Beneš, N., Křetínský, J., Larsen, K.G., Møller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inf. 52(2–3), 269–297 (2015)

    Article  MathSciNet  MATH  Google Scholar 

  37. Beneš, N., Křetínský, J., Larsen, K.G., Srba, J.: Checking thorough refinement on modal transition systems is EXPTIME-complete. In: Leucker, M., Morgan, C. (eds.) [LM09], pp. 112–126

    Google Scholar 

  38. 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)

    Article  MathSciNet  MATH  Google Scholar 

  39. 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)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  41. Bauer, S.S., Larsen, K.G., Legay, A., Nyman, U., Wasowski, A.: A modal specification theory for components with data. Sci. Comput. Program. 83, 106–128 (2014)

    Article  Google Scholar 

  42. 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 2009. LNCS, vol. 5885, pp. 679–697. Springer, Heidelberg (2009). doi:10.1007/978-3-642-10373-5_35

    Chapter  Google Scholar 

  43. 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)

    Article  MATH  Google Scholar 

  44. Børjesson, A., Larsen, K.G., Skou, A.: Generality in design and compositional verification using TAV. Formal Methods Syst. Des. 6(3), 239–258 (1995)

    Article  Google Scholar 

  45. Bauer, S.S., Mayer, P., Legay, A.: MIO workbench: a tool for compositional design with modal input/output interfaces. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 418–421. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24372-1_30

    Chapter  Google Scholar 

  46. Bauer, S.S., Mayer, P., Schroeder, A., Hennicker, R.: On weak modal compatibility, refinement, and the MIO workbench. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 175–189. Springer, Heidelberg (2010). doi:10.1007/978-3-642-12002-2_15

    Chapter  Google Scholar 

  47. 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 2009. LNCS, vol. 5457, pp. 152–163. Springer, Heidelberg (2009). doi:10.1007/978-3-642-00982-2_13

    Chapter  Google Scholar 

  48. Bruns, G.: An industrial application of modal process logic. Sci. Comput. Program. 29(1–2), 3–22 (1997)

    Article  Google Scholar 

  49. Bujtor, F., Sorokin, L., Vogler, W.: Testing preorders for DMTS: deadlock- and the new deadlock/divergence-testing. In: 15th International Conference on Application of Concurrency to System Design, ACSD 2015, Brussels, Belgium, 21–26 June 2015, pp. 60–69. IEEE Computer Society (2015)

    Google Scholar 

  50. Bujtor, F., Vogler, W.: Failure semantics for modal transition systems. ACM Trans. Embed. Comput. Syst. 14(4), 67:1–67:30 (2015)

    Article  Google Scholar 

  51. Chatterjee, K., Doyen, L.: Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 599–610. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14162-1_50

    Chapter  Google Scholar 

  52. Chakrabarti, A., Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45212-6_9

    Chapter  Google Scholar 

  53. Chechik, M., Devereux, B., Easterbrook, S.M., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371–408 (2003)

    Article  MATH  Google Scholar 

  54. 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. IEEE Computer Society (2010)

    Google Scholar 

  55. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). doi:10.1007/BFb0025774

    Chapter  Google Scholar 

  56. Chatterjee, K., Gaiser, A., Křetínský, J.: Automata with generalized rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 559–575. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_37

    Chapter  Google Scholar 

  57. Čerāns, K., Godskesen, J.C., Larsen, K.G.: Timed modal specification—theory and tools. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 253–267. Springer, Heidelberg (1993). doi:10.1007/3-540-56922-7_21

    Chapter  Google Scholar 

  58. Campetelli, A., Gruler, A., Leucker, M., Thoma, D.: Don’t know for multi-valued systems. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 289–305. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_22

    Chapter  Google Scholar 

  59. Caillaud, B., Raclet, J.-B.: Ensuring reachability by design. In: Roychoudhury, A., D’Souza, M. (eds.) [RD12], pp. 213–227

    Google Scholar 

  60. Carbone, M., Sobocinski, P., Valencia, F.D.: Foreword: Festschrift for mogens nielsen’s 60th birthday. Theor. Comput. Sci. 410(41), 4001–4005 (2009)

    Article  MathSciNet  Google Scholar 

  61. Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: LICS, pp. 195–204. IEEE (2012)

    Google Scholar 

  62. de Alfaro, L., Godefroid, P., Jagadeesan, R.: Three-valued abstractions of games: uncertainty, but with precision. In: LICS04 [LIC04], pp. 170–179

    Google Scholar 

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

    Google Scholar 

  64. D’Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: The modal transition system control problem. In: Giannakopoulou, D., Méry, D. (eds.) [GM12], pp. 155–170

    Google Scholar 

  65. Darondeau, P., Dubreil, J., Marchand, H.: Supervisory control for modal specifications of services. In: WODES, pp. 428–435 (2010)

    Google Scholar 

  66. D’Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S.: MTSA: the modal transition system analyser. In: ASE, pp. 475–476. IEEE (2008)

    Google Scholar 

  67. D’Ippolito, N., Fischbein, D., Foster, H., Uchitel, S.: MTSA: eclipse support for modal transition systems construction, analysis and elaboration. In: Cheng, L.-T., Orso, A., Robillard, M.P. (eds.) ETX, pp. 6–10. ACM (2007)

    Google Scholar 

  68. Delahaye, B., Fahrenberg, U., Larsen, K.G., Legay, A.: Refinement and difference for probabilistic automata. Log. Methods Comput. Sci. 10(3) (2014)

    Google Scholar 

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

    Article  Google Scholar 

  70. Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wąsowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 324–339. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18275-4_23

    Chapter  Google Scholar 

  71. Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: New results on abstract probabilistic automata. In: Caillaud, B., Carmona, J., Hiraishi, K. (eds.) 11th International Conference on Application of Concurrency to System Design, ACSD 2011, Newcastle Upon Tyne, UK, 20–24 June 2011, pp. 118–127. IEEE Computer Society (2011)

    Google Scholar 

  72. David, A., Larsen, K.G., Legay, A., Nyman, U., Wąsowski, A.: ECDAR: an environment for compositional design and analysis of real time systems. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol. 6252, pp. 365–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15643-4_29

    Chapter  Google Scholar 

  73. Delahaye, B., Larsen, K.G., Legay, A., Pedersen, M.L., Wasowski, A.: APAC: a tool for reasoning about abstract probabilistic automata. In: Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5–8 September 2011, pp. 151–152. IEEE Computer Society (2011)

    Google Scholar 

  74. Delahaye, B., Larsen, K.G., Legay, A.: Stuttering for abstract probabilistic automata. J. Log. Algebr. Program. 83(1), 1–19 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  75. D’Argenio, P.R., Melgratti, H. (eds.): CONCUR 2013. LNCS, vol. 8052. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40184-8

    MATH  Google Scholar 

  76. Dams, D., Namjoshi, K.S.: The existence of finite abstractions for branching time model checking. In: LICS04 [LIC04], pp. 335–344

    Google Scholar 

  77. Diskin, Z., Safilian, A., Maibaum, T., Ben-David, S.: Faithful modeling of product lines with kripke structures and modal logic. Sci. Ann. Comput. Sci. 26(1), 69–122 (2016)

    MathSciNet  MATH  Google Scholar 

  78. Elhog-Benzina, D., Haddad, S., Hennicker, R.: Process refinement and asynchronous composition with modalities. In: Donatelli, S., Kleijn, J., Machado, R.J., Fernandes, J.M. (eds.) ACSD/Petri Nets Workshops. CEUR Workshop Proceedings, vol. 827, pp. 385–401. CEUR-WS.org (2010)

    Google Scholar 

  79. Elhog-Benzina, D., Haddad, S., Hennicker, R.: Refinement and asynchronous composition of modal petri nets. Trans. Petri Nets Other Models Concurr. 5, 96–120 (2012)

    Article  MATH  Google Scholar 

  80. Esparza, J., Křetínský, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192–208. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_13

    Google Scholar 

  81. Fischbein, D., Braberman, V.A., Uchitel, S.: A sound observational semantics for modal transition systems. In: Leucker, M., Morgan, C. (eds.) [LM09], pp. 215–230

    Google Scholar 

  82. Fischbein, D.: Foundations for behavioural model elaboration using modal transition systems. Ph.D. thesis, Imperial College London, UK, (2012)

    Google Scholar 

  83. Fahrenberg, U., Křetínský, J., Legay, A., Traonouez, L.-M.: Compositionality for quantitative specifications. In: Lanese, I., Madelaine, E. (eds.) [LM15], pp. 306–324

    Google Scholar 

  84. Fahrenberg, U., Legay, A.: A robust specification theory for modal event-clock automata. In: Bauer, S.S., Raclet, J.-B. (eds) FIT. EPTCS, vol. 87, pp. 5–16 (2012)

    Google Scholar 

  85. Fahrenberg, U., Legay, A.: General quantitative specification theories with modal transition systems. Acta Inf. 51(5), 261–295 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  86. Fahrenberg, U., Legay, A., Traonouez, L.-M.: Structural refinement for the modal nu-Calculus. In: Ciobanu, G., Méry, D. (eds.) ICTAC 2014. LNCS, vol. 8687, pp. 169–187. Springer, Cham (2014). doi:10.1007/978-3-319-10882-7_11

    Google Scholar 

  87. Fecher, H., Leucker, M., Wolf, V.: Don’t know in probabilistic systems. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 71–88. Springer, Heidelberg (2006). doi:10.1007/11691617_5

    Chapter  Google Scholar 

  88. Feuillade, G., Pinchinat, S.: Modal specifications for the control theory of discrete event systems. Discret. Event Dyn. Syst. 17(2), 211–232 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  89. Fecher, H., Steffen, M.: Characteristic \(\mu \)-calculus formulas for underspecified transition systems. Electr. Notes Theor. Comput. Sci. 128(2), 103–116 (2005)

    Article  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  91. Fischbein, D., Uchitel, S.: On correct and complete strong merging of partial behaviour models. In: Harrold, M.J., Murphy, G.C. (eds.) SIGSOFT FSE, pp. 297–307. ACM (2008)

    Google Scholar 

  92. Guerra, P.T., Andrade, A., Wassermann, R.: Toward the revision of CTL models through Kripke modal transition systems. In: Iyoda, J., Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 115–130. Springer, Heidelberg (2013). doi:10.1007/978-3-642-41071-0_9

    Chapter  Google Scholar 

  93. Gurfinkel, A., Chechik, M.: Why waste a perfectly good abstraction? In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 212–226. Springer, Heidelberg (2006). doi:10.1007/11691372_14

    Chapter  Google Scholar 

  94. Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001). doi:10.1007/3-540-44685-0_29

    Chapter  Google Scholar 

  95. Godefroid, P., Jagadeesan, R.: On the expressiveness of 3-valued models. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 206–222. Springer, Heidelberg (2003). doi:10.1007/3-540-36384-X_18

    Chapter  Google Scholar 

  96. Giannakopoulou, D., Méry, D. (eds.): FM 2012. LNCS, vol. 7436. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32759-9

    MATH  Google Scholar 

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

    Google Scholar 

  98. Godefroid, P., Piterman, N.: LTL generalized model checking revisited. In: Jones, N.D., Müller-Olm, M. (eds.) [JMO09], pp. 89–104

    Google Scholar 

  99. Gawlick, R., Segala, R., Søgaard-Andersen, J., Lynch, N.: Liveness in timed and untimed systems. In: Abiteboul, S., Shamir, E. (eds.) ICALP 1994. LNCS, vol. 820, pp. 166–177. Springer, Heidelberg (1994). doi:10.1007/3-540-58201-0_66

    Chapter  Google Scholar 

  100. Gurfinkel, A., Wei, O., Chechik, M.: Systematic construction of abstractions for model-checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 381–397. Springer, Heidelberg (2005). doi:10.1007/11609773_25

    Chapter  Google Scholar 

  101. Gurfinkel, A., Wei, O., Chechik, M.: Yasm: a software model-checker for verification and refutation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 170–174. Springer, Heidelberg (2006). doi:10.1007/11817963_18

    Chapter  Google Scholar 

  102. Hennessy, M.: Acceptance trees. J. ACM 32(4), 896–928 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  103. Hussain, A., Huth, M.: On model checking multiple hybrid views. Theor. Comput. Sci. 404(3), 186–201 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  104. Haddad, S., Hennicker, R., Møller, M.H.: Specification of asynchronous component systems with modal I/O-petri nets. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 219–234. Springer, Cham (2014). doi:10.1007/978-3-319-05119-2_13

    Chapter  Google Scholar 

  105. Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: a foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 155–169. Springer, Heidelberg (2001). doi:10.1007/3-540-45309-1_11

    Chapter  Google Scholar 

  106. Hermanns, H., Krčál, J., Křetínský, J.: Compositional verification and optimization of interactive Markov chains. In: D’Argenio, P.R., Melgratti, H.C. (eds.) [DM13], pp. 364–379

    Google Scholar 

  107. Han, T., Krause, C., Kwiatkowska, M.Z., Giese, H.: Modal specifications for probabilistic timed systems. In: Bortolussi, L., Wiklicky, H. (eds.) QAPL. EPTCS, vol. 117, pp. 66–80 (2013)

    Google Scholar 

  108. Hüttel, H., Larsen, K.G.: The use of static constructs in a model process logic. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 163–180. Springer, Heidelberg (1989). doi:10.1007/3-540-51237-3_14

    Chapter  Google Scholar 

  109. Holmström, S.: A refinement calculus for specifications in Hennessy-Milner logic with recursion. Formal Asp. Comput. 1(3), 242–272 (1989)

    Article  MATH  Google Scholar 

  110. Huth, M.: A unifying framework for model checking labeled kripke structures, modal transition systems, and interval transition systems. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 369–380. Springer, Heidelberg (1999). doi:10.1007/3-540-46691-6_30

    Chapter  Google Scholar 

  111. Huth, M.: Model checking modal transition systems using Kripke structures. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 302–316. Springer, Heidelberg (2002). doi:10.1007/3-540-47813-2_21

    Chapter  Google Scholar 

  112. Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266–277. IEEE Computer Society (1991)

    Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  114. Jones, N.D., Müller-Olm, M. (eds.): VMCAI 2009. LNCS, vol. 5403. Springer, Heidelberg (2009). doi:10.1007/978-3-540-93900-9

    Google Scholar 

  115. Juhl, L.: Quantities in games and modal transition systems. Ph.D. thesis, Department of Computer Science, Aalborg University (2013)

    Google Scholar 

  116. Krka, I., D’Ippolito, N., Medvidović, N., Uchitel, S.: Revisiting compatibility of input-output modal transition systems. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 367–381. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_26

    Chapter  Google Scholar 

  117. Komárková, Z., Křetínský, J.: Rabinizer 3: safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 235–241. Springer, Cham (2014). doi:10.1007/978-3-319-11936-6_17

    Google Scholar 

  118. Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time Markov chains. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 311–324. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_37

    Chapter  Google Scholar 

  119. Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81(4), 356–389 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  120. Krka I., Medvidovic, N.: Revisiting modal interface automata. In: Gnesi, S., Gruner, S., Plat, N., Rumpe, B. (eds.) Proceedings of the First International Workshop on Formal Methods in Software Engineering - Rigorous and Agile Approaches, FormSERA 2012, Zurich, Switzerland, 2 June 2012, pp. 30–36. IEEE (2012)

    Google Scholar 

  121. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  122. Kozen, D.: Results on the propositional \(\mu \)-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  123. Křetínský, J.: Modal transition systems: extensions and analysis. Ph.D. thesis, Masaryk University, Brno, Department of Computer Science (2014)

    Google Scholar 

  124. Křetínský, M., Řehák, V., Strejček, J.: Reachability of Hennessy-Milner properties for weakly extended PRS. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 213–224. Springer, Heidelberg (2005). doi:10.1007/11590156_17

    Chapter  Google Scholar 

  125. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990)

    Article  MathSciNet  MATH  Google Scholar 

  126. Křetínský, J., Sickert, S.: MoTraS: a tool for modal transition systems and their extensions. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 487–491. Springer, Cham (2013). doi:10.1007/978-3-319-02444-8_41

    Chapter  Google Scholar 

  127. Křetínský, J., Sickert, S.: On refinements of Boolean and parametric modal transition systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 213–230. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39718-9_13

    Chapter  Google Scholar 

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

  129. Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232–246. Springer, Heidelberg (1990). doi:10.1007/3-540-52148-8_19

    Chapter  Google Scholar 

  130. Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability +. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33–56. Springer, Heidelberg (1990). doi:10.1007/BFb0039050

    Chapter  Google Scholar 

  131. 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14–17 July 2004, Turku, Finland, Proceedings. IEEE Computer Society (2004)

    Google Scholar 

  132. Larsen, K.G., Legay, A.: Quantitative modal transition systems. In: Martí-Oliet, N., Palomino, M. (eds.) WADT 2012. LNCS, vol. 7841, pp. 50–58. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37635-1_3

    Chapter  Google Scholar 

  133. Leucker, M., Morgan, C. (eds.): ICTAC 2009. LNCS, vol. 5684. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03466-4

    MATH  Google Scholar 

  134. Lanese, I., Madelaine, E. (eds.): FACS 2014. LNCS, vol. 8997. Springer, Cham (2015). doi:10.1007/978-3-319-15317-9

    Google Scholar 

  135. Luthmann, L., Mennicke, S., Lochau, M.: Towards an I/O conformance testing theory for software product lines based on modal interface automata. In: Atlee, J.M., Gnesi, S. (eds.) Proceedings 6th Workshop on Formal Methods and Analysis in SPL Engineering, FMSPLE@ETAPS 2015, London, UK, 11 April 2015. EPTCS, vol. 182, pp. 1–13 (2015)

    Google Scholar 

  136. Larsen, K.G., Nyman, U., Wąsowski, A.: Modal I/O automata for interface and product line theories. In: Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 64–79. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71316-6_6

    Chapter  Google Scholar 

  137. Larsen, K.G., Nyman, U., Wąsowski, A.: On modal refinement and consistency. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 105–119. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74407-8_8

    Chapter  Google Scholar 

  138. Larsen, K.G., Steffen, B., Weise, C.: Fischer’s protocol revisited: a simple proof using modal constraints. In: Alur, R., Henzinger, T.A., Sontag, E.D. (eds.) HS 1995. LNCS, vol. 1066, pp. 604–615. Springer, Heidelberg (1996). doi:10.1007/BFb0020979

    Chapter  Google Scholar 

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

    Google Scholar 

  140. Lüttgen, G., Vogler, W.: Modal interface automata. Log. Methods Comput. Sci. 9(3) (2013)

    Google Scholar 

  141. Lüttgen, G., Vogler, W., Fendrich, S.: Richer interface automata with optimistic and pessimistic compatibility. Acta Inf. 52(4–5), 305–336 (2015)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  143. Manta, A.: Implementation of algorithms for modal transition systems with durations. Bachelor’s thesis, Technische Universität München (2013)

    Google Scholar 

  144. Mayr, R.: Process rewrite systems. Inf. Comput. 156(1–2), 264–286 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  145. Møller, M.H.: Modal and component-based system specifications. Ph.D. thesis, Department of Computer Science, Aalborg University (2013)

    Google Scholar 

  146. Motras. http://www7.in.tum.de/kretinsk/motras.html

  147. Namjoshi, K.S.: Abstraction for branching time properties. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 288–300. Springer, Heidelberg (2003). doi:10.1007/978-3-540-45069-6_29

    Chapter  Google Scholar 

  148. Nanz, S., Nielson, F., Riis Nielson, H.: Modal abstractions of concurrent behaviour. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 159–173. Springer, Heidelberg (2008). doi:10.1007/978-3-540-69166-2_11

    Chapter  Google Scholar 

  149. Nyman, U.: Modal transition systems as the basis for interface theories and product lines. Ph.D. thesis, Aalborg Universitet (2008)

    Google Scholar 

  150. Pnueli, A. The temporal logic of programs. In: FOCS, pp. 46–57. IEEE Computer Society (1977)

    Google Scholar 

  151. Piterman, N., Pnueli, A.: Faster solutions of Rabin and Streett games. In: LICS, pp. 275–284. IEEE Computer Society (2006)

    Google Scholar 

  152. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179–190. ACM Press (1989)

    Google Scholar 

  153. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  154. Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). doi:10.1007/3-540-11494-7_22

    Chapter  Google Scholar 

  155. Raclet, J.-B.: Quotient de spécifications pour la réutilisation de composants. Ph.D. thesis, Université de Rennes I (2007). (In French)

    Google Scholar 

  156. Raclet, J.-B.: Residual for component specifications. Electr. Notes Theor. Comput. Sci. 215, 93–110 (2008)

    Article  Google Scholar 

  157. Raclet, J.-B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: Modal interfaces: unifying interface automata and modal specifications. In:Chakraborty, S., Halbwachs, N., (eds.) EMSOFT, pp. 87–96. ACM (2009)

    Google Scholar 

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

    Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  160. Roychoudhury, A., D’Souza, M. (eds.): ICTAC 2012. LNCS, vol. 7521. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32943-2

    MATH  Google Scholar 

  161. Sibay, G.E., Braberman, V.A., Uchitel, S., Kramer, J.: Synthesizing modal transition systems from triggered scenarios. IEEE Trans. Softw. Eng. 39(7), 975–1001 (2013)

    Article  Google Scholar 

  162. Schlachter, U.: Bounded petri net synthesis from modal transition systems is undecidable. In: Desharnais, J., Jagadeesan, R. (eds.), 27th International Conference on Concurrency Theory, CONCUR 2016, Québec City, Canada, 23–26 August 2016. LIPIcs, vol. 59, pp. 15:1–15:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)

    Google Scholar 

  163. Sassolas, M., Chechik, M., Uchitel, S.: Exploring inconsistencies between modal transition systems. Softw. Syst. Model. 10(1), 117–142 (2011)

    Article  Google Scholar 

  164. Shoham, S., Grumberg, O.: Monotonic abstraction-refinement for CTL. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 546–560. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_40

    Chapter  Google Scholar 

  165. Siirtola, A., Heljanko, K.: Parametrised modal interface automata. ACM Trans. Embed. Comput. Syst. 14(4), 65:1–65:25 (2015)

    Article  Google Scholar 

  166. Sharma, A., Katoen, J.-P.: Layered reduction for abstract probabilistic automata. In: 14th International Conference on Application of Concurrency to System Design, ACSD 2014, Tunis La Marsa, Tunisia, 23–27 June 2014, pp. 21–31. IEEE Computer Society (2014)

    Google Scholar 

  167. Sibay, G.E., Uchitel, S., Braberman, V.A., Kramer, J.: Distribution of modal transition systems. In: Giannakopoulou, D., Méry, D. (eds.) [GM12], pp. 403–417

    Google Scholar 

  168. Beek, M.H., Damiani, F., Gnesi, S., Mazzanti, F., Paolini, L.: From featured transition systems to modal transition systems with variability constraints. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 344–359. Springer, Cham (2015). doi:10.1007/978-3-319-22969-0_24

    Chapter  Google Scholar 

  169. ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Modelling and analysing variability in product families: model checking of modal transition systems with variability constraints. J. Log. Algebr. Meth. Program. 85(2), 287–315 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  170. Uchitel, S., Brunet, G., Chechik, M.: Behaviour model synthesis from properties and scenarios. In: ICSE, pp. 34–43. IEEE Computer Society (2007)

    Google Scholar 

  171. Uchitel, S., Brunet, G., Chechik, M.: Synthesis of partial behavior models from properties and scenarios. IEEE Trans. Softw. Eng. 35(3), 384–406 (2009)

    Article  Google Scholar 

  172. Uchitel, S., Chechik, M.: Merging partial behavioural models. In: Taylor, R.N., Dwyer, M.B. (eds.) SIGSOFT FSE, pp. 43–52. ACM (2004)

    Google Scholar 

  173. Verdier, G., Raclet, J.-B.: Maccs: a tool for reachability by design. In: Lanese, I., Madelaine, E. (eds.) [LM15], pp. 191–197

    Google Scholar 

  174. Verdier, G., Raclet, J.-B.: Quotient of acceptance specifications under reachability constraints. In: Dediu, A.-H., Formenti, E., Martín-Vide, C., Truthe, B. (eds.) LATA 2015. LNCS, vol. 8977, pp. 299–311. Springer, Cham (2015). doi:10.1007/978-3-319-15579-1_23

    Google Scholar 

  175. Walukiewicz, I.: Pushdown processes: games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 62–74. Springer, Heidelberg (1996). doi:10.1007/3-540-61474-5_58

    Chapter  Google Scholar 

  176. Wei, O., Gurfinkel, A., Chechik, M.: Mixed transition systems revisited. In: Jones, N.D., Müller-Olm, M. (eds.) [JMO09], pp. 349–365

    Google Scholar 

Download references

Acknowledgement

I would like to thank Kim G. Larsen for introducing me to the topic of MTS and research in general, the pleasant collaboration during my Erasmus stay as a Master student at AAU a decade ago and ever since then. Arriving to Aalborg right after the paper 20 Years of Modal and Mixed Specifications [AHL+08a] was published, my first paper with Kim [BKLS09b] was on MTS as a part of the Festschrift to Mogens Nielsen’s 60th birthday [CSV09]. It is a pleasure and an honour to contribute today to Kim’s Festschrift.

Author information

Authors and Affiliations

  1. Technical University of Munich, Munich, Germany

    Jan Křetínský

Authors
  1. Jan Křetínský
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Křetínský .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Luca Aceto

  2. Aalborg University, Aalborg, Denmark

    Giorgio Bacci

  3. Aalborg University, Aalborg, Denmark

    Giovanni Bacci

  4. Reykjavík University, Reykjavik, Iceland

    Anna Ingólfsdóttir

  5. Inria Campus Beaulieu, Rennes, France

    Axel Legay

  6. Aalborg University, Aalborg, Denmark

    Radu Mardare

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Křetínský, J. (2017). 30 Years of Modal Transition Systems: Survey of Extensions and Analysis. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63121-9_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63120-2

  • Online ISBN: 978-3-319-63121-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics