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.
@InProceedings{bocchi_et_al:LIPIcs.CONCUR.2015.283, author = {Bocchi, Laura and Lange, Julien and Yoshida, Nobuko}, title = {{Meeting Deadlines Together}}, booktitle = {26th International Conference on Concurrency Theory (CONCUR 2015)}, pages = {283--296}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-91-0}, ISSN = {1868-8969}, year = {2015}, volume = {42}, editor = {Aceto, Luca and de Frutos Escrig, David}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.283}, URN = {urn:nbn:de:0030-drops-53838}, doi = {10.4230/LIPIcs.CONCUR.2015.283}, annote = {Keywords: timed automata, multiparty session types, global specification} }
Feedback for Dagstuhl Publishing