Bocchi, Laura, Yoshida, Nobuko, Lange, Julien (2015) Meeting Deadlines Together. In: Aceto, Luca and de Frutos-Escrig, David, eds. International Conference on Concurrency Theory (CONCUR). Leibniz International Proceedings in Informatics . pp. 283-296. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik ISBN 978-3-939897-91-0. (doi:10.4230/LIPIcs.CONCUR.2015.283) (KAR id:50257)
PDF
Pre-print
Language: English |
|
Download this file (PDF/833kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.283 |
Abstract
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.
Item Type: | Conference or workshop item (Paper) |
---|---|
DOI/Identification number: | 10.4230/LIPIcs.CONCUR.2015.283 |
Subjects: |
Q Science > QA Mathematics (inc Computing science) > QA150 Algebra Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, > QA76.76 Computer software |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Laura Bocchi |
Date Deposited: | 21 Aug 2015 09:05 UTC |
Last Modified: | 10 Dec 2022 23:10 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/50257 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):