2026-07-27T21:43:46Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5383 2024-03-06T10:36:31Z ddc:004 open_access

Meeting Deadlines Together Bocchi, Laura Lange, Julien Yoshida, Nobuko timed automata multiparty session types global specification This paper studies safety, progress, and non-zeno properties of Communicating Timed Automata (CTAs), which are timed automata (TA) extended with unbounded communication channels, and presents a procedure to build timed global specifications from systems of CTAs. We define safety and progress properties for CTAs by extending properties studied in communicating finite-state machines to the timed setting. We then study non-zenoness for CTAs; our aim is to prevent scenarios in which the participants have to execute an infinite number of actions in a finite amount of time. We propose sound and decidable conditions for these properties, and demonstrate the practicality of our approach with an implementation and experimental evaluations of our theory. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Laura Bocchi and Julien Lange and Nobuko Yoshida 2015 Is Part Of LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2015.283 urn:nbn:de:0030-drops-53838 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.283 eng https://creativecommons.org/licenses/by/3.0/legalcode