Skip to main content

The Least Fibred Lifting and the Expressivity of Coalgebraic Modal Logic

  • Conference paper

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

Abstract

Every endofunctor B on the category Set can be lifted to a fibred functor on the category (fibred over Set) of equivalence relations and relation-preserving functions. In this paper, the least (fibre-wise) of such liftings, L(B), is characterized for essentially any B. The lifting has all the useful properties of the relation lifting due to Jacobs, without the usual assumption of weak pullback preservation; if B preserves weak pullbacks, the two liftings coincide. Equivalence relations can be viewed as Boolean algebras of subsets (predicates, tests). This correspondence relates L(B) to the least test suite lifting T(B), which is defined in the spirit of predicate lifting as used in coalgebraic modal logic. Properties of T(B) translate to a general expressivity result for a modal logic for B-coalgebras. In the resulting logic, modal operators of any arity can appear.

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

Buying options

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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theoretical Computer Science 249, 3–80 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  2. Park, D.M.: Concurrency and automata on infinite sequences. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 195–219. Springer, Heidelberg (1982)

    Google Scholar 

  3. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1988)

    Google Scholar 

  4. Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Information and Computation 145, 107–152 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  5. Jacobs, B.: Exercises in coalgebraic specification. In: Blackhouse, R., Crole, R.L., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Jacobs, B., Hughes, J.: Simulations in coalgebra. Electronic Notes in Theoretical Computer Science 82 (2003)

    Google Scholar 

  7. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32, 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  8. Jacobs, B.: Towards a duality result in the modal logic for coalgebras. In: Proc. CMCS 2000. Electronic Notes in Theoretical Computer Science, vol. 33 (2000)

    Google Scholar 

  9. Klin, B.: Abstract Coalgebraic Approach to Process Equivalence for Well-Behaved Operational Semantics. PhD thesis, BRICS, Aarhus University (2004)

    Google Scholar 

  10. Moss, L.: Coalgebraic logic. Annals of Pure and Applied Logic 96, 177–317 (1999)

    Article  MathSciNet  Google Scholar 

  11. Pattinson, D.: Expressivity Results in the Modal Logic of Coalgebras. PhD thesis, Universität München (2001)

    Google Scholar 

  12. Pattinson, D.: Semantical principles in the modal logic of coalgebras. In: Ferreira, A., Reichel, H. (eds.) STACS 2001. LNCS, vol. 2010, p. 514. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Schröder, L.: Expressivity of coalgebraic modal logic: the limits and beyond. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 440–454. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  14. Jacobs, B.: Trace semantics for coalgebras. In: Proc. CMCS 2004. Electronic Notes in Theoretical Computer Science, vol. 106 (2004)

    Google Scholar 

  15. Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999)

    MATH  Google Scholar 

  16. Aczel, P., Mendler, N.: A final coalgebra theorem. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 357–365. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  17. Thomsen, B.: A theory of higher-order communicating systems. Information and Computation 116 (1995)

    Google Scholar 

  18. Cirstea, C., Pattinson, D.: Modular construction of modal logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 258–275. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klin, B. (2005). The Least Fibred Lifting and the Expressivity of Coalgebraic Modal Logic. In: Fiadeiro, J.L., Harman, N., Roggenbach, M., Rutten, J. (eds) Algebra and Coalgebra in Computer Science. CALCO 2005. Lecture Notes in Computer Science, vol 3629. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11548133_16

Download citation

  • DOI: https://doi.org/10.1007/11548133_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28620-2

  • Online ISBN: 978-3-540-31876-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics