Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Proving Behavioural Apartness

  • Conference paper
  • First Online:
Coalgebraic Methods in Computer Science (CMCS 2024)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14617))

Included in the following conference series:

  • 90 Accesses

Abstract

Bisimilarity is a central notion for coalgebras. In recent work, Geuvers and Jacobs suggest to focus on apartness, which they define by dualising coalgebraic bisimulations. This yields the possibility of finite proofs of distinguishability for a wide variety of state-based systems.

We propose behavioural apartness, defined by dualising behavioural equivalence rather than bisimulations. A motivating example is the subdistribution functor, where the proof system based on bisimilarity requires an infinite quantification over couplings, whereas behavioural apartness instantiates to a finite rule. In addition, we provide optimised proof rules for behavioural apartness and show their use in several examples.

This research is partially supported by the NWO grant No. OCENW.M20.053, the EPSRC NIA Grant EP/X019373/1, and the Royal Society Travel Grant IES\(\backslash \) R3\(\backslash \)223092 and the Leverhulme Trust Research Project Grant RPG-2020-232.

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
$34.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

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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

Similar content being viewed by others

References

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

    Chapter  Google Scholar 

  2. Barlocco, S., Kupke, C., Rot, J.: Coalgebra learning via duality. In: Bojańczyk, M., Simpson, A. (eds.) FoSSaCS 2019. LNCS, vol. 11425, pp. 62–79. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17127-8_4

    Chapter  Google Scholar 

  3. Basold, H.: Mixed inductive-coinductive reasoning types, programs and logic. Ph.D. thesis, Radboud Universiteit Nijmegen (2018)

    Google Scholar 

  4. Beohar, H., Gurke, S., König, B., Messing, K.: Hennessy-Milner theorems via Galois connections. In: CSL. LIPIcs, vol. 252, pp. 12:1–12:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

    Google Scholar 

  5. Beohar, H., et al.: Expressive quantale-valued logics for coalgebras: an adjunction-based approach. In: STACS. LIPIcs, vol. 289, pp. 10:1–10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2024)

    Google Scholar 

  6. Blok, A.: Interaction, observation and denotation. Master’s thesis, Universiteit van Amsterdam (2012)

    Google Scholar 

  7. Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 407–421. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46678-0_26

    Chapter  Google Scholar 

  8. Desharnais, J., Edalat, A., Panangaden, P.: Bisimulation for labelled Markov processes. Inf. Comput. 179(2), 163–193 (2002)

    Article  MathSciNet  Google Scholar 

  9. Fijalkow, N., Klin, B., Panangaden, P.: Expressiveness of probabilistic modal logics, revisited. In: ICALP. LIPIcs, vol. 80, pp. 105:1–105:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  10. Forster, J., Goncharov, S., Hofmann, D., Nora, P., Schröder, L., Wild, P.: Quantitative Hennessy-Milner theorems via notions of density. In: CSL. LIPIcs, vol. 252, pp. 22:1–22:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)

    Google Scholar 

  11. Geuvers, H.: Apartness and distinguishing formulas in Hennessy-Milner logic. In: Jansen, N., Stoelinga, M., van den Bos, P. (eds.) A Journey from Process Algebra via Timed Automata to Model Learning. LNCS, vol. 13560, pp. 266–282. Springer, Cham (2022). https://doi.org/10.1007/978-3-031-15629-8_14

    Chapter  Google Scholar 

  12. Geuvers, H., Jacobs, B.: Relating apartness and bisimulation. Log. Methods Comput. Sci. 17(3) (2021)

    Google Scholar 

  13. Goncharov, S., Hofmann, D., Nora, P., Schröder, L., Wild, P.: Kantorovich functors and characteristic logics for behavioural distances. In: Kupferman, O., Sobocinski, P. (eds.) FoSSaCS 2023. LNCS, vol. 13992, pp. 46–67. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30829-1_3

    Chapter  Google Scholar 

  14. Gumm, H.P.: Elements of the general theory of coalgebras. In: LUATCS 99. Rand Afrikaans University, South Africa (1999)

    Google Scholar 

  15. Gumm, H.P.: Copower functors. Theor. Comput. Sci. 410(12–13), 1129–1142 (2009)

    Article  MathSciNet  Google Scholar 

  16. Gumm, H.P., Schröder, T.: Monoid-labeled transition systems. In: CMCS. Electronic Notes in Theoretical Computer Science, vol. 44, pp. 185–204. Elsevier (2001)

    Google Scholar 

  17. Hasuo, I., Kataoka, T., Cho, K.: Coinductive predicates and final sequences in a fibration. Math. Struct. Comput. Sci. 28(4), 562–611 (2018)

    Article  MathSciNet  Google Scholar 

  18. Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998)

    Article  MathSciNet  Google Scholar 

  19. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press, Cambridge (2016)

    Google Scholar 

  20. Katsumata, S., Sato, T., Uustalu, T.: Codensity lifting of monads and its dual. Log. Methods Comput. Sci. 14(4) (2018)

    Google Scholar 

  21. Komorida, Y., et al.: Codensity games for bisimilarity. New Gener. Comput. 40(2), 403–465 (2022)

    Article  Google Scholar 

  22. Komorida, Y., Katsumata, S., Kupke, C., Rot, J., Hasuo, I.: Expressivity of quantitative modal logics: categorical foundations via codensity and approximation. In: LICS, pp. 1–14. IEEE (2021)

    Google Scholar 

  23. König, B., Mika-Michalski, C.: (Metric) bisimulation games and real-valued modal logics for coalgebras. In: CONCUR. LIPIcs, vol. 118, pp. 37:1–37:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018)

    Google Scholar 

  24. König, B., Mika-Michalski, C., Schröder, L.: Explaining non-bisimilarity in a coalgebraic approach: games and distinguishing formulas. In: Petrişan, D., Rot, J. (eds.) CMCS 2020. LNCS, vol. 12094, pp. 133–154. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-57201-3_8

    Chapter  Google Scholar 

  25. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MathSciNet  Google Scholar 

  26. Lucanu, D., Goriac, E.-I., Caltais, G., Roşu, G.: CIRC: a behavioral verification tool based on circular coinduction. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 433–442. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03741-2_30

    Chapter  Google Scholar 

  27. Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Log. 96(1–3), 277–317 (1999)

    Article  MathSciNet  Google Scholar 

  28. Schröder, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2–3), 230–247 (2008)

    Article  MathSciNet  Google Scholar 

  29. Sokolova, A.: Coalgebraic analysis of probabilistic systems. Ph.D. thesis (2005)

    Google Scholar 

  30. Sokolova, A.: Probabilistic systems coalgebraically: a survey. Theor. Comput. Sci. 412(38), 5095–5110 (2011)

    Article  MathSciNet  Google Scholar 

  31. Sprunger, D., Katsumata, S., Dubut, J., Hasuo, I.: Fibrational bisimulations and quantitative reasoning: extended version. J. Log. Comput. 31(6), 1526–1559 (2021)

    Article  MathSciNet  Google Scholar 

  32. Sprunger, D., Moss, L.S.: Precongruences and parametrized coinduction for logics for behavioral equivalence. In: CALCO. LIPIcs, vol. 72, pp. 23:1–23:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)

    Google Scholar 

  33. Staton, S.: Relating coalgebraic notions of bisimulation. Log. Methods Comput. Sci. 7(1) (2011)

    Google Scholar 

  34. de Vink, E.P., Rutten, J.J.M.M.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theor. Comput. Sci. 221(1–2), 271–293 (1999)

    Article  MathSciNet  Google Scholar 

  35. Wißmann, T., Milius, S., Katsumata, S., Dubut, J.: A coalgebraic view on reachability (2020)

    Google Scholar 

  36. Wißmann, T., Milius, S., Schröder, L.: Quasilinear-time computation of generic modal witnesses for behavioural inequivalence. Log. Methods Comput. Sci. 18(4) (2022)

    Google Scholar 

  37. Worrell, J.: On the final sequence of a finitary set functor. Theor. Comput. Sci. 338(1–3), 184–199 (2005)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Radboud University, Nijmegen, Netherlands

    Ruben Turkenburg & Jurriaan Rot

  2. University of Sheffield, Sheffield, UK

    Harsh Beohar

  3. Strathclyde University, Glasgow, UK

    Clemens Kupke

Authors
  1. Ruben Turkenburg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Harsh Beohar
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Clemens Kupke
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jurriaan Rot
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ruben Turkenburg .

Editor information

Editors and Affiliations

  1. University of Duisburg-Essen, Duisburg, Germany

    Barbara König

  2. FAU Erlangen-Nürnberg, Erlangen, Germany

    Henning Urbat

Rights and permissions

Reprints and permissions

Copyright information

© 2024 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Turkenburg, R., Beohar, H., Kupke, C., Rot, J. (2024). Proving Behavioural Apartness. In: König, B., Urbat, H. (eds) Coalgebraic Methods in Computer Science. CMCS 2024. Lecture Notes in Computer Science, vol 14617. Springer, Cham. https://doi.org/10.1007/978-3-031-66438-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-66438-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-66437-3

  • Online ISBN: 978-3-031-66438-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Societies and partnerships

Search

Navigation