Advertisement

Algebraic-Coalgebraic Specification in CoCasl

  • Till Mossakowski
  • Horst Reichel
  • Markus Roggenbach
  • Lutz Schröder
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2755)

Abstract

We introduce CoCasl as a simple coalgebraic extension of the algebraic specification language Casl. CoCasl allows the nested combination of algebraic datatypes and coalgebraic process types. We show that the well-known coalgebraic modal logic can be expressed in CoCasl. We present sufficient criteria for the existence of cofree models, also for several variants of nested cofree and free specifications. Moreover, we describe an extension of the existing proof support for Casl (in the shape of an encoding into higher-order logic) to CoCasl.

Keywords

Modal Logic Partial Algebra Modal Formula Type Construct Atomic Sentence 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Adámek, J., Herrlich, H., Strecker, G.E.: Abstract and concrete categories. Wiley Interscience, Hoboken (1990)zbMATHGoogle Scholar
  2. 2.
    Arbib, M., Manes, E.: Parametrized data types do not need highly constrained parameters. Inform. Control 52, 139–158 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Barr, M.: Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci. 114, 299–315 (1993)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Bidoit, M., Hennicker, R.: On the integration of observability and reachability concepts. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 21–36. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Bidoit, M., Hennicker, R., Kurz, A.: Observational logic, constructor-based logic, and their duality. Theoret. Comput. Sci. 298, 471–510 (2003)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Burmeister, P.: Partial algebras – survey of a unifying approach towards a twovalued model theory for partial algebras. Algebra Universalis 15, 306–358 (1982)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Cîrstea, C.: On specification logics for algebra-coalgebra structures: Reconciling reachability and observability. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 82–97. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Cockett, R., Fukushima, T.: About Charity, Yellow Series Report 92/480/18, Univ. of Calgary, Dept. of Comp. Sci. (1992)Google Scholar
  9. 9.
    Jones, S.P., et al.: Haskell 98: A non-strict, purely functional language (1999), http://www.haskell.org/onlinereport
  10. 10.
    Goguen, J., Lin, K., Rosu, G.: Conditional circular coinductive rewriting. In: Automated Software Engineering, pp. 123–131. IEEE Press, Los Alamitos (2000)Google Scholar
  11. 11.
    Goguen, J.A.: Hidden algebraic engineering. In: Nehaniv, C., Ito, M. (eds.) Algebraic Engineering, pp. 17–36. World Scientific, Singapore (1999)Google Scholar
  12. 12.
    Gumm, H.P., Schröder, T.: Coalgebras of bounded type. Math. Struct. Comput. Sci. 12, 565–578 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Kozen, D.: Results on the propositional mu -calculus. Theoret. Comput. Sci. 27, 333–354 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Kurz, A.: Specifying coalgebras with modal logic. Theoret. Comput. Sci. 260, 119–138 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Kurz, A.: Logics admitting final semantics. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 238–249. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Mossakowski, T.: Casl: From semantics to tools. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 93–108. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  17. 17.
    Mossakowski, T.: Relating Casl with other specification languages: the institution level. Theoret. Comput. Sci. 286, 367–475 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Mossakowski, T., Roggenbach, M., Schröder, L.: CoCasl at work – modelling process algebra. In: CMCS 2003. ENTCS, vol. 82(1) (2003)Google Scholar
  19. 19.
    Mossakowski, T., Schröder, L., Roggenbach, M., Reichel, H.: Algebraic-coalgebraic specification in CoCasl, Tech. report, University of Bremen, available at http://www.informatik.uni-bremen.de/~lschrode/papers/cocasl.ev.ps
  20. 20.
    Mosses, P.D. (ed.): Casl – the common algebraic specification language. Reference manual. Springer, Heidelberg (to appear)Google Scholar
  21. 21.
    Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction, Tech. report, LMU München (2002)Google Scholar
  22. 22.
    Reichel, H.: An approach to object semantics based on terminal co-algebras. Math. Struct. Comput. Sci. 5, 129–152 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Reichel, H.: A uniform model theory for the specification of data and process types. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 348–365. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  24. 24.
    Roşu, G.: Hidden logic, Ph.D. thesis, Univ. of California at San Diego (2000)Google Scholar
  25. 25.
    Rothe, J., Tews, H., Jacobs, B.: The Coalgebraic Class Specification Language CCSL. J. Universal Comput. Sci. 7, 175–193 (2001)MathSciNetzbMATHGoogle Scholar
  26. 26.
    Rutten, J.: Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249, 3–80 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Tarlecki, A.: On the existence of free models in abstract algebraic institutions. Theoret. Comput. Sci. 37, 269–304 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Tews, H.: Coalgebraic methods for object–oriented languages, Ph.D. thesis, Dresden Univ. of Technology (2002)Google Scholar
  29. 29.
    van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Till Mossakowski
    • 1
  • Horst Reichel
    • 2
  • Markus Roggenbach
    • 1
  • Lutz Schröder
    • 1
  1. 1.BISS, Dept. of Computer ScienceUniversity of BremenGermany
  2. 2.Institute for Theoretical Computer ScienceTechnical University of DresdenGermany

Personalised recommendations