Skip to main content
SpringerLink
Log in

A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories

  • Conference paper
  • First Online:
Book cover SOFSEM 2017: Theory and Practice of Computer Science (SOFSEM 2017)

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

Abstract

We propose behavioral specification theories for most equivalences in the linear-time–branching-time spectrum. Almost all previous work on specification theories focuses on bisimilarity, but there is a clear interest in specification theories for other preorders and equivalences. We show that specification theories for preorders cannot exist and develop a general scheme which allows us to define behavioral specification theories, based on disjunctive modal transition systems, for most equivalences in the linear-time–branching-time spectrum.

Most of this work was carried out while the first author was still employed at Inria Rennes, France.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

References

  1. Aceto, L., Fábregas, I., de Frutos-Escrig, D., Ingólfsdóttir, A., Palomino, M.: On the specification of modal systems. Sci. Comput. Program. 78(12), 2468–2487 (2013)

    Article  Google Scholar 

  2. Aceto, L., Fokkink, W., van Glabbeek, R.J., Ingólfsdóttir, A.: Nested semantics over finite trees are equationally hard. Inf. Comput. 191(2), 203–232 (2004)

    Article  MathSciNet  MATH  Google Scholar 

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

    MathSciNet  MATH  Google Scholar 

  4. 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 

  5. Bauer, S.S., Fahrenberg, U., Juhl, L., Larsen, K.G., Legay, A., Thrane, C.: Weighted modal transition systems. Form. Meth. Syst. Design 42(2), 193–220 (2013)

    Article  MATH  Google Scholar 

  6. 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 

  7. 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, Berlin (2011). doi:10.1007/978-3-642-24372-1_17

    Chapter  Google Scholar 

  8. Bertrand, N., Legay, A., Pinchinat, S., Raclet, J.: Modal event-clock specifications for timed component-based design. Sci. Comput. Program. 77(12), 1212–1234 (2012)

    Article  MATH  Google Scholar 

  9. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  10. Bujtor, F., Sorokin, L., Vogler, W.: Testing preorders for dMTS: deadlock- and the new deadlock/divergence-testing. In: IEEE Computer Society, ACSD (2015)

    Google Scholar 

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

    Article  Google Scholar 

  12. Caillaud, B., Raclet, J.-B.: Ensuring reachability by design. In: Roychoudhury, A., D’Souza, M. (eds.) ICTAC 2012. LNCS, vol. 7521, pp. 213–227. Springer, Berlin (2012). doi:10.1007/978-3-642-32943-2_17

    Chapter  Google Scholar 

  13. David, A., Larsen, K.G., Legay, A., Nyman, U., Traonouez, L., Wasowski, A.: Real-time specifications. STTT 17(1), 17–45 (2015)

    Article  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Fahrenberg, U., Legay, A.: The quantitative linear-time-branching-time spectrum. Theor. Comput. Sci. 538, 54–69 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  16. Fahrenberg, U., Legay, A.: A linear-time branching-time spectrum of behavioral specification theories (2016). http://arxiv.org/abs/1604.06503

  17. Groote, J.F., Vaandrager, F.W.: Structured operational semantics and bisimulation as a congruence. Inf. Comput. 100(2), 202–260 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  18. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  MATH  Google Scholar 

  20. Larsen, K.G.: A context dependent equivalence between processes. Theor. Comput. Sci. 49, 184–215 (1987)

    Article  MATH  Google Scholar 

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

    Chapter  Google Scholar 

  22. 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, Heielberg (1990). doi:10.1007/BFb0039050

    Chapter  Google Scholar 

  23. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. In: POPL, ACM Press (1989)

    Google Scholar 

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

    Google Scholar 

  25. Milner, R.: Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  26. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). doi:10.1007/BFb0017309

    Chapter  Google Scholar 

  27. Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985). doi:10.1007/BFb0015727

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Article  Google Scholar 

  30. Stirling, C.: Modal and temporal logics for processes. In Banff Higher Order Workshop. LNCS, 1043. Springer, Heidelberg (1995)

    Google Scholar 

  31. van Glabbeek, R.J.: The linear time - branching time spectrum I. In: Handbook of Process Algebra, Chap. 1. Elsevier (2001)

    Google Scholar 

  32. Vogler, W.: Failures semantics and deadlocking of modular Petri nets. Acta Inf. 26(4), 333–348 (1989)

    MathSciNet  MATH  Google Scholar 

  33. Vogler, W.: Modular Construction and Partial Order Semantics of Petri Nets. LNCS, vol. 625. Springer, Heidelberg (1992)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. École polytechnique, Palaiseau, France

    Uli Fahrenberg

  2. Inria, Rennes, France

    Axel Legay

Authors
  1. Uli Fahrenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Axel Legay
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Uli Fahrenberg .

Editor information

Editors and Affiliations

  1. TU Dortmund , Dortmund, Germany

    Bernhard Steffen

  2. TU Dresden , Dresden, Germany

    Christel Baier

  3. Eindhoven University of Technology , Eindhoven, The Netherlands

    Mark van den Brand

  4. Alpen Adria University Klagenfurt , Klagenfurt, Austria

    Johann Eder

  5. Lero - Irish Software Research Center , Limerick, Ireland

    Mike Hinchey

  6. Lero - Irish Software Research Center , Limerick, Ireland

    Tiziana Margaria

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Fahrenberg, U., Legay, A. (2017). A Linear-Time–Branching-Time Spectrum of Behavioral Specification Theories. In: Steffen, B., Baier, C., van den Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds) SOFSEM 2017: Theory and Practice of Computer Science. SOFSEM 2017. Lecture Notes in Computer Science(), vol 10139. Springer, Cham. https://doi.org/10.1007/978-3-319-51963-0_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51963-0_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51962-3

  • Online ISBN: 978-3-319-51963-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation