×

zbMATH — the first resource for mathematics

Input urgent semantics for asynchronous timed session types. (English) Zbl 1431.68078
Summary: We study an urgent semantics of asynchronous timed session types, where input actions happen as soon as possible, inspired to common programming primitives. We introduce a notion of asynchronous compliance for timed session types, ensuring deadlock freedom and eventual reception. As in the untimed case, asynchronous compliance is undecidable. We then show that synchronous compliance, shown decidable in previous work, is a sound approximation of asynchronous compliance.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing
Software:
Diogenes; Uppaal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] The go programming language
[2] Alur, Rajeev; Dill, David L., A theory of timed automata, Theor. Comput. Sci., 126, 2, 183-235, (1994) · Zbl 0803.68071
[3] Atzei, Nicola; Bartoletti, Massimo, Developing honest java programs with diogenes, (FORTE 2016. FORTE 2016, LNCS, vol. 9688, (2016), Springer), 52-61
[4] Barbanera, Franco; de’Liguoro, Ugo, Sub-behaviour relations for session-based client/server systems, Math. Struct. Comput. Sci., 25, 6, 1339-1381, (2015) · Zbl 1361.68159
[5] Bartoletti, Massimo; Bocchi, Laura; Murgia, Maurizio, Progress-preserving refinements of CTA, (CONCUR. CONCUR, LIPIcs, vol. 118, (2018), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 40:1-40:19
[6] Bartoletti, Massimo; Cimoli, Tiziana; Murgia, Maurizio, Timed session types, Log. Methods Comput. Sci., 13, 4, (2017) · Zbl 1398.68356
[7] Bartoletti, Massimo; Cimoli, Tiziana; Murgia, Maurizio; Podda, Alessandro Sebastian; Pompianu, Livio, A contract-oriented middleware, (FACS. FACS, LNCS, vol. 9539, (2015), Springer), 86-104
[8] Bartoletti, Massimo; Murgia, Maurizio; Scalas, Alceste; Zunino, Roberto, Verifiable abstractions for contract-oriented systems, J. Log. Algebraic Methods Program., 86, 1, 159-207, (2017) · Zbl 1353.68194
[9] Bartoletti, Massimo; Scalas, Alceste; Zunino, Roberto, A semantic deconstruction of session types, (Proc. CONCUR. Proc. CONCUR, LNCS, vol. 8704, (2014), Springer), 402-418 · Zbl 1417.68115
[10] Basu, Samik; Bultan, Tevfik, On deciding synchronizability for asynchronously communicating systems, Theor. Comput. Sci., 656, 60-75, (2016) · Zbl 1353.68195
[11] Behrmann, Gerd; David, Alexandre; Larsen, Kim G., A tutorial on Uppaal, (Formal Methods for the Design of Real-Time Systems. Formal Methods for the Design of Real-Time Systems, LNCS, vol. 3185, (2004), Springer), 200-236 · Zbl 1105.68350
[12] Berthomieu, Bernard; Diaz, Michel, Modeling and verification of time dependent systems using time petri nets, IEEE Trans. Softw. Eng., 17, 3, 259-273, (1991)
[13] Bocchi, Laura; Lange, Julien; Yoshida, Nobuko, Meeting deadlines together, (CONCUR. CONCUR, LIPIcs, vol. 42, (2015), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 283-296 · Zbl 1374.68320
[14] Bocchi, Laura; Murgia, Maurizio; Thudichum Vasconcelos, Vasco; Yoshida, Nobuko, Asynchronous timed session types - from duality to time-sensitive processes, (ESOP. ESOP, Lecture Notes in Computer Science, vol. 11423, (2019), Springer), 583-610
[15] Bocchi, Laura; Yang, Weizhen; Yoshida, Nobuko, Timed multiparty session types, (CONCUR. CONCUR, LNCS, vol. 8704, (2014), Springer), 419-434 · Zbl 1417.68117
[16] Bornot, Sébastien; Sifakis, Joseph; Tripakis, Stavros, Modeling urgency in timed systems, (COMPOS. COMPOS, LNCS, vol. 1536, (1997), Springer), 103-129
[17] Bouajjani, Ahmed; Enea, Constantin; Ji, Kailiang; Qadeer, Shaz, On the completeness of verifying message passing programs under bounded asynchrony, (CAV (2). CAV (2), Lecture Notes in Computer Science, vol. 10982, (2018), Springer), 372-391
[18] Brand, Daniel; Zafiropulo, Pitro, On communicating finite-state machines, J. ACM, 30, 2, 323-342, (1983) · Zbl 0512.68039
[19] Castagna, Giuseppe; Dezani-Ciancaglini, Mariangiola; Giachino, Elena; Padovani, Luca, Foundations of session types, (PPDP, (2009), ACM), 219-230
[20] Castagna, Giuseppe; Gesbert, Nils; Padovani, Luca, A theory of contracts for web services, ACM Trans. Program. Lang. Syst., 31, 5, (2009) · Zbl 1295.68080
[21] Dezani-Ciancaglini, Mariangiola; de’Liguoro, Ugo, Sessions and session types: An overview, (WS-FM. WS-FM, LNCS, vol. 6194, (2009), Springer), 1-28
[22] Finkel, Alain; Lozes, Étienne, Synchronizability of communicating finite state machines is not decidable, (ICALP. ICALP, LIPIcs, vol. 80, (2017), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 122:1-122:14
[23] Honda, Kohei; Thudichum Vasconcelos, Vasco; Kubo, Makoto, Language primitives and type discipline for structured communication-based programming, (ESOP. ESOP, LNCS, vol. 1381, (1998), Springer), 122-138
[24] Honda, Kohei; Yoshida, Nobuko; Carbone, Marco, Multiparty asynchronous session types, J. ACM, 63, 1, 9:1-9:67, (2016) · Zbl 1426.68047
[25] Krcál, Pavel; Yi, Wang, Communicating timed automata: the more synchronous, the more difficult to verify, (CAV. CAV, LNCS, vol. 4144, (2006), Springer), 249-262 · Zbl 1188.68192
[26] Lange, Julien; Tuosto, Emilio; Yoshida, Nobuko, From communicating machines to graphical choreographies, (POPL, (2015), ACM), 221-232 · Zbl 1346.68136
[27] Lange, Julien; Yoshida, Nobuko, On the undecidability of asynchronous session subtyping, (FOSSACS. FOSSACS, LNCS, vol. 10203, (2017)), 441-457 · Zbl 06721005
[28] Murgia, Maurizio, On urgency in asynchronous timed session types, (ICE, (2018))
[29] Neykova, Rumyana; Bocchi, Laura; Yoshida, Nobuko, Timed runtime monitoring for multiparty conversations, Form. Asp. Comput., 29, 5, 877-910, (2017) · Zbl 1375.68030
[30] Nicollin, Xavier; Sifakis, Joseph, An overview and synthesis on timed process algebras, (CAV, (1991)), 376-398
[31] Catuscia, Palamidessi, Comparing the expressive power of the synchronous and asynchronous pi-calculi, Math. Struct. Comput. Sci., 13, 5, 685-719, (2003)
[32] Takeuchi, Kaku; Honda, Kohei; Kubo, Makoto, An interaction-based language and its typing system, (PARLE. PARLE, LNCS, vol. 817, (1994), Springer), 398-413
[33] Yi, Wang, CCS + time = an interleaving model for real time systems, (ICALP. ICALP, Lecture Notes in Computer Science, vol. 510, (1991), Springer), 217-228 · Zbl 0769.68027
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.