Skip to main content
Kent Academic Repository

Asynchronous Subtyping by Trace Relaxation

Bocchi, Laura and King, Andy and Murgia, Maurizio (2023) Asynchronous Subtyping by Trace Relaxation. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture notes in computer science, 14570 . Springer, pp. 207-226. (In press) (doi:10.1007/978-3-031-57246-3_12) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:105395)

Language: English

Restricted to Repository staff only

Contact us about this Publication
[thumbnail of main.pdf]
Official URL:


Session subtyping answers the question of whether a program in a communicating system can be safely substituted for another, when their communication behaviours are described by session types. Asynchronous session subtyping is undecidable, hence the interest in devising sound, although incomplete, subtyping algorithms. State-of-the-art algorithms are formulated in terms of a data-structure called input trees. We show how input trees can be replaced by sets of traces, which opens up opportunities for applying techniques abstract interpretation techniques to the problem of asynchronous session subtyping. Sets of traces can be relaxed (enlarged) whilst still allowing subtyping to be observed, and one can choose relaxations that can be finitely represented, even when the input trees are arbitrarily large. We instantiate this strategy using regular expressions and show that it allows subtyping to be mechanically proven for communication patterns that were previously out of reach.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-031-57246-3_12
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 21 Mar 2024 10:53 UTC
Last Modified: 22 Mar 2024 14:50 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Bocchi, Laura.

Creator's ORCID:
CReDIT Contributor Roles:

King, Andy.

Creator's ORCID:
CReDIT Contributor Roles:

Murgia, Maurizio.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.