MobilityReadingGroup

Meeting Deadlines Together

Laura BOCCHI, Julien LANGE, Nobuko YOSHIDA

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 the 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{BLY2015,
  author = {Laura Bocchi and Julien Lange and Nobuko Yoshida},
  title = {{Meeting Deadlines Together}},
  booktitle = {26th International Conference on Concurrency Theory},
  series = {LIPIcs},
  volume = {42},
  pages = {283--296},
  publisher = {Schloss Dagstuhl},
  year = 2015
}

@inproceedings{BLY2015,
  author = {Laura Bocchi and Julien Lange and Nobuko Yoshida},
  title = {{Meeting Deadlines Together}},
  booktitle = {26th International Conference on Concurrency Theory},
  series = {LIPIcs},
  volume = {42},
  pages = {283--296},
  publisher = {Schloss Dagstuhl},
  doi = "10.4230/LIPIcs.CONCUR.2015.283",
  year = 2015
}