Published: 17th September 2020|
|Preface Julien Lange, Anastasia Mavridou, Larisa Safina and Alceste Scalas|
|On the k-synchronizability of Distributed Systems Cinzia Di Giusto||1|
|Parity Games: The Quasi-polynomial Era Karoliina Lehtinen||2|
|A type language for message passing component-based systems Zorica Savanović, Letterio Galletta and Hugo Torres Vieira||3|
|Typestates to Automata and back: a tool André Trindade, João Mota and António Ravara||25|
|An Abstract Framework for Choreographic Testing Alex Coto, Roberto Guanciale and Emilio Tuosto||43|
|Towards Refinable Choreographies Ugo de'Liguoro, Hernán Melgratti and Emilio Tuosto||61|
|On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency Ronny Tredup and Evgeny Erofeev||78|
This volume contains the proceedings of ICE'20, the 13th Interaction and Concurrency Experience, which was held online (due to the COVID-19 pandemic) as a satellite event of DisCoTec'20. The previous editions of ICE were affiliated with ICALP'08 (Reykjavik, Iceland), CONCUR'09 (Bologna, Italy), DisCoTec'10 (Amsterdam, The Netherlands), DisCoTec'11 (Reykjavik, Iceland), DisCoTec'12 (Stockholm, Sweden), DisCoTec'13 (Florence, Italy), DisCoTec'14 (Berlin, Germany), DisCoTec'15 (Grenoble, France), DisCoTec'16 (Heraklion, Greece), DisCoTec'17 (Neuchâtel, Switzerland), DisCoTec'18 (Madrid, Spain), and DisCoTec'19 (Lyngby, Denmark).
The ICE workshop series features a distinguishing review and selection procedure: PC members are encouraged to interact, anonymously, with authors. This year these interactions took place on the OpenReview platform which combines paper selection features with forum-like interactions. As in the past editions, the forum discussion during the review and selection phase of ICE'20 considerably improved the accuracy of the feedback from the reviewers and the quality of accepted papers, and offered the basis for lively discussion during the workshop. The time and effort spent on the interaction between reviewers and authors is rewarding for all parties. The discussions on OpenReview make it possible to resolve misunderstandings at an early stage of the review process, to discover and correct mistakes in key definitions, and to improve examples and presentation.
The 2020 edition of ICE included double blind reviewing of original research papers, in order to increase fairness and avoid bias in reviewing. Research papers were blinded for submission, with authors' names and identifying details removed, and authors were given anonymous access to a dedicated section of OpenReview. Each paper was reviewed by three PC members, and altogether 5 papers were accepted for publication — plus 5 oral presentations which are not part of this volume. We were proud to host 2 invited talks, by Cinzia Di Giusto and Karoliina Lehtinen. The abstracts of these talks are included in this volume, together with the final versions of the research papers, which take into account the discussion at the workshop.
We would like to thank the authors of all the submitted papers for their interest in the workshop. We thank Cinzia Di Giusto and Karoliina Lehtinen for accepting our invitations to present their recent work. We are grateful for the efforts of the PC members:
We thank the ICE steering committee and the DisCoTec'20 organizers, in particular the general and workshop chairs, for providing an excellent environment for the preparation and staging of the event: a remarkable feat, especially considering the challenging circumstances due to the COVID-19 pandemic. Finally, we thank the editors of EPTCS for the publication of these post-proceedings.
I will discuss the notion of k-synchronizability: a system is k-synchronizable if any of its executions, up to reordering causally independent actions, can be divided into a succession of k-bounded interaction phases. We know that the reachability problem is decidable for k-synchronizable systems. Moreover, the membership problem (whether a system is k-synchronizable for a given k) is decidable as well. Our proofs fix several important issues in previous attempts to prove these two results for mailbox automata. Finally, I will point our last results on deciding whether there exists a k such that a system is k-synchronizable.
Parity games are central to the verification and synthesis of reactive systems: various model-checking and synthesis problems reduce to solving these games. Solving parity games -- that is, deciding which player has a winning strategy -- is one of the few problems known to be in both UP and co-UP yet not known to be in P. So far, the quest for a polynomial algorithm has lasted over 25 years.
In 2017 a major breakthrough occurred: parity games are solvable in quasi-polynomial time. Since then, several seemingly very distinct quasi-polynomial algorithms have been published, both by myself and others, and some of the novel ideas behind them have been applied to address other verification problems.
This talk takes you on a high-level tour of what has been going on in the world of parity games since 2017 and where we are now. I will present one particularly straight-forward quasi-polynomial algorithm in more detail.