Proving behavioural apartness

Ruben Turkenburg; Harsh Beohar; Clemens Kupke; Jurriaan Rot

doi:10.1007/978-3-031-66438-0_8

Proving behavioural apartness

Ruben Turkenburg^*, Harsh Beohar, Clemens Kupke, Jurriaan Rot

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

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.

Original language	English
Title of host publication	Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings
Editors	Barbara König, Henning Urbat
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	156-173
Number of pages	18
ISBN (Electronic)	978-3-031-66438-0
ISBN (Print)	9783031664373
DOIs	https://doi.org/10.1007/978-3-031-66438-0_8
Publication status	Published - Aug 2024
Event	17th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2024 - Luxembourg City, Luxembourg Duration: 6 Apr 2024 → 7 Apr 2024

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14617 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	17th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2024
Country/Territory	Luxembourg
City	Luxembourg City
Period	6/04/24 → 7/04/24

Funding

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\ R3\ 223092 and the Leverhulme Trust Research Project Grant RPG-2020-232.

Keywords

coalgebras
behavioural equivalence

Access to Document

10.1007/978-3-031-66438-0_8

Cite this

Turkenburg, R., Beohar, H., Kupke, C., & Rot, J. (2024). Proving behavioural apartness. In B. König, & H. Urbat (Eds.), Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings (pp. 156-173). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14617 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-66438-0_8

Turkenburg, Ruben ; Beohar, Harsh ; Kupke, Clemens et al. / Proving behavioural apartness. Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings. editor / Barbara König ; Henning Urbat. Springer Science and Business Media Deutschland GmbH, 2024. pp. 156-173 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ac13cb5fe3ec41708d4ce5cf9e06df19,

title = "Proving behavioural apartness",

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.",

keywords = "coalgebras, behavioural equivalence",

author = "Ruben Turkenburg and Harsh Beohar and Clemens Kupke and Jurriaan Rot",

year = "2024",

month = aug,

doi = "10.1007/978-3-031-66438-0_8",

language = "English",

isbn = "9783031664373",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "156--173",

editor = "Barbara K{\"o}nig and Henning Urbat",

booktitle = "Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings",

address = "Germany",

note = "17th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2024 ; Conference date: 06-04-2024 Through 07-04-2024",

}

Turkenburg, R, Beohar, H, Kupke, C & Rot, J 2024, Proving behavioural apartness. in B König & H Urbat (eds), Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14617 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 156-173, 17th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2024, Luxembourg City, Luxembourg, 6/04/24. https://doi.org/10.1007/978-3-031-66438-0_8

Proving behavioural apartness. / Turkenburg, Ruben; Beohar, Harsh; Kupke, Clemens et al.
Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings. ed. / Barbara König; Henning Urbat. Springer Science and Business Media Deutschland GmbH, 2024. p. 156-173 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14617 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution book

TY - GEN

T1 - Proving behavioural apartness

AU - Turkenburg, Ruben

AU - Beohar, Harsh

AU - Kupke, Clemens

AU - Rot, Jurriaan

PY - 2024/8

Y1 - 2024/8

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

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

KW - coalgebras

KW - behavioural equivalence

UR - https://arxiv.org/abs/2404.16588

U2 - 10.1007/978-3-031-66438-0_8

DO - 10.1007/978-3-031-66438-0_8

M3 - Conference contribution book

AN - SCOPUS:85200653519

SN - 9783031664373

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 156

EP - 173

BT - Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings

A2 - König, Barbara

A2 - Urbat, Henning

PB - Springer Science and Business Media Deutschland GmbH

T2 - 17th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2024

Y2 - 6 April 2024 through 7 April 2024

ER -

Turkenburg R, Beohar H, Kupke C, Rot J. Proving behavioural apartness. In König B, Urbat H, editors, Coalgebraic Methods in Computer Science - 17th IFIP WG 1.3 International Workshop, CMCS 2024, Colocated with ETAPS 2024, Proceedings. Springer Science and Business Media Deutschland GmbH. 2024. p. 156-173. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2024 Jul 26. doi: 10.1007/978-3-031-66438-0_8

Proving behavioural apartness

Abstract

Publication series

Conference

Funding

Keywords

Access to Document

Other files and links

Fingerprint

Cite this