5 Search Results for "Jongmans, Sung-Shik"

Document
DOI: 10.4230/LIPIcs.FSTTCS.2025.52
Unreliability in Practical Subclasses of Communicating Systems

Authors: Amrita Suresh and Nobuko Yoshida

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract
Systems of communicating automata are prominent models for peer-to-peer message-passing over unbounded channels, but in the general scenario, most verification properties are undecidable. To address this issue, two decidable subclasses, Realisable with Synchronous Communication (RSC) and k-Multiparty Compatibility (k-MC), were proposed in the literature, with corresponding verification tools developed and applied in practice. Unfortunately, both RSC and k-MC are not resilient under failures: (1) their decidability relies on the assumption of perfect channels and (2) most standard protocols do not satisfy RSC or k-MC under failures. To address these limitations, this paper studies the resilience of RSC and k-MC under two distinct failure models: interference and crash-stop failures. For interference, we relax the conditions of RSC and k-MC and prove that the inclusions of these relaxed properties remain decidable under interference, preserving their known complexity bounds. We then propose a novel crash-handling communicating system that captures wider behaviours than existing multiparty session types (MPST) with crash-stop failures. We study a translation of MPST with crash-stop failures into this system integrating RSC and k-MC properties, and establish their decidability results. Finally, by verifying representative protocols from the literature using RSC and k-MC tools extended to interferences, we evaluate the relaxed systems and demonstrate their resilience.
Cite as

Amrita Suresh and Nobuko Yoshida. Unreliability in Practical Subclasses of Communicating Systems. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 52:1-52:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{suresh_et_al:LIPIcs.FSTTCS.2025.52,
  author =	{Suresh, Amrita and Yoshida, Nobuko},
  title =	{{Unreliability in Practical Subclasses of Communicating Systems}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{52:1--52:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.52},
  URN =		{urn:nbn:de:0030-drops-251312},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.52},
  annote =	{Keywords: Communicating automata, lossy channel, corruption, out of order, session types, crash-stop failure}
}
Document
Pearl/Brave New Idea
DOI: 10.4230/LIPIcs.ECOOP.2023.42
Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea)

Authors: Sung-Shik Jongmans and Francisco Ferreira

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications. In this paper, we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically. Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. We present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before).
Cite as

Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Pearl/Brave New Idea). In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 42:1-42:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{jongmans_et_al:LIPIcs.ECOOP.2023.42,
  author =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  title =	{{Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{42:1--42:30},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.42},
  URN =		{urn:nbn:de:0030-drops-182358},
  doi =		{10.4230/LIPIcs.ECOOP.2023.42},
  annote =	{Keywords: behavioural types, multiparty session types, choreographies}
}
Document
Artifact
DOI: 10.4230/DARTS.9.2.18
Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)

Authors: Sung-Shik Jongmans and Francisco Ferreira

Published in: DARTS, Volume 9, Issue 2, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
Programming distributed systems is difficult. Multiparty session typing (MPST) is a method to automatically prove safety and liveness of protocol implementations relative to protocol specifications. In the related article ("Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types", in ECOOP 2023, LIPIcs, Vol. 263, pp. 42:1-42:30), we introduce two new techniques to significantly improve the expressiveness of the MPST method: projection is based on implicit local types instead of explicit; type checking is based on the operational semantics of implicit local types instead of on the syntax. That is, the reduction relation on implicit local types is used not only "a posteriori" to prove type soundness (as usual), but also "a priori" to define the typing rules - synthetically. Classes of protocols that can now be specified/implemented/verified for the first time using the MPST method include: recursive protocols in which different roles participate in different branches; protocols in which a receiver chooses the sender of the first communication; protocols in which multiple roles synchronously choose both the sender and the receiver of a next communication, implemented as mixed input/output processes. In the related article, we present the theory of the new techniques, as well as their future potential, and we demonstrate their present capabilities to effectively support regular expressions as global types (not possible before). As evidence that the new techniques are implementable, we implemented them; this implementation is available in this artifact.
Cite as

Sung-Shik Jongmans and Francisco Ferreira. Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 18:1-18:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Article{jongmans_et_al:DARTS.9.2.18,
  author =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  title =	{{Synthetic Behavioural Typing: Sound, Regular Multiparty Sessions via Implicit Local Types (Artifact)}},
  pages =	{18:1--18:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2023},
  volume =	{9},
  number =	{2},
  editor =	{Jongmans, Sung-Shik and Ferreira, Francisco},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.9.2.18},
  URN =		{urn:nbn:de:0030-drops-182580},
  doi =		{10.4230/DARTS.9.2.18},
  annote =	{Keywords: behavioural types, multiparty session types, choreographies}
}
Document
Artifact
DOI: 10.4230/DARTS.8.2.19
API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact)

Authors: Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença

Published in: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Construction and analysis of distributed systems is difficult. Multiparty session types (MPST) constitute a method to make it easier. The idea is to use type checking to statically prove deadlock freedom and protocol compliance of communicating processes. In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. With this artifact, and the companion paper, we revisit and revise this approach. Regarding our "revisitation", using Scala 3, we present the existing API generation approach, which is based on deterministic finite automata (DFA), in terms of both the existing states-as-classes encoding of DFAs as APIs, and a new states-as-type-parameters encoding; the latter leverages match types in Scala 3. Regarding our "revision", also using Scala 3, we present a new API generation approach that is based on sets of pomsets instead of DFAs; it crucially leverages match types, too. Our fresh perspective allows us to avoid two forms of combinatorial explosion resulting from implementing concurrent subprotocols in the DFA-based approach. We implement our approach in a new API generation tool, called Pompset. This artifact contains Pompset.
Cite as

Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 19:1-19:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{cledou_et_al:DARTS.8.2.19,
  author =	{Cledou, Guillermina and Edixhoven, Luc and Jongmans, Sung-Shik and Proen\c{c}a, Jos\'{e}},
  title =	{{API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3 (Artifact)}},
  pages =	{19:1--19:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Cledou, Guillermina and Edixhoven, Luc and Jongmans, Sung-Shik and Proen\c{c}a, Jos\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.8.2.19},
  URN =		{urn:nbn:de:0030-drops-162171},
  doi =		{10.4230/DARTS.8.2.19},
  annote =	{Keywords: Concurrency, pomsets (partially ordered multisets), match types, Scala 3}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2022.27
API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3

Authors: Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença

Published in: LIPIcs, Volume 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022)

Abstract
Construction and analysis of distributed systems is difficult. Multiparty session types (MPST) constitute a method to make it easier. The idea is to use type checking to statically prove deadlock freedom and protocol compliance of communicating processes. In practice, the premier approach to apply the MPST method in combination with mainstream programming languages has been based on API generation. In this paper (pearl), we revisit and revise this approach. Regarding our "revisitation", using Scala 3, we present the existing API generation approach, which is based on deterministic finite automata (DFA), in terms of both the existing states-as-classes encoding of DFAs as APIs, and a new states-as-type-parameters encoding; the latter leverages match types in Scala 3. Regarding our "revision", also using Scala 3, we present a new API generation approach that is based on sets of pomsets instead of DFAs; it crucially leverages match types, too. Our fresh perspective allows us to avoid two forms of combinatorial explosion resulting from implementing concurrent subprotocols in the DFA-based approach. We implement our approach in a new API generation tool.
Cite as

Guillermina Cledou, Luc Edixhoven, Sung-Shik Jongmans, and José Proença. API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 27:1-27:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{cledou_et_al:LIPIcs.ECOOP.2022.27,
  author =	{Cledou, Guillermina and Edixhoven, Luc and Jongmans, Sung-Shik and Proen\c{c}a, Jos\'{e}},
  title =	{{API Generation for Multiparty Session Types, Revisited and Revised Using Scala 3}},
  booktitle =	{36th European Conference on Object-Oriented Programming (ECOOP 2022)},
  pages =	{27:1--27:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-225-9},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{222},
  editor =	{Ali, Karim and Vitek, Jan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2022.27},
  URN =		{urn:nbn:de:0030-drops-162559},
  doi =		{10.4230/LIPIcs.ECOOP.2022.27},
  annote =	{Keywords: Concurrency, pomsets (partially ordered multisets), match types, Scala 3}
}
  • Refine by Type
  • 5 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2023
  • 2 2022

  • Refine by Author
  • 4 Jongmans, Sung-Shik
  • 2 Cledou, Guillermina
  • 2 Edixhoven, Luc
  • 2 Ferreira, Francisco
  • 2 Proença, José
  • Show More...

  • Refine by Series/Journal
  • 3 LIPIcs
  • 2 DARTS

  • Refine by Classification
  • 3 Theory of computation → Concurrency
  • 2 Software and its engineering → Software notations and tools
  • 1 Theory of computation → Automata extensions
  • 1 Theory of computation → Distributed computing models

  • Refine by Keyword
  • 2 Concurrency
  • 2 Scala 3
  • 2 behavioural types
  • 2 choreographies
  • 2 match types
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact