{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T11:39:18Z","timestamp":1742384358902},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,12,1]],"date-time":"2006-12-01T00:00:00Z","timestamp":1164931200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2006,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Zeno-timelocks constitute a challenge for the formal verification of timed automata: they are difficult to detect, and the verification of most properties (e.g., safety) is only correct for timelock-free models. Some time ago, Tripakis proposed a syntactic check on the structure of timed automata: if a certain condition (called strong non-zenoness\u2019 SNZ) is met by all the loops in a given automaton, then zeno-timelocks are guaranteed not to occur. Checking for SNZ is efficient, and compositional (if all components in a network of automata are strongly non-zeno, then the network is free from zeno-timelocks). Strong non-zenoness, however, is sufficient-only: There exist non-zeno specifications which are not strongly non-zeno. A TCTL formula is known that represents a sufficient-and-necessary condition for non-zenoness; unfortunately, this formula requires a demanding model-checking algorithm, and not all model-checkers are able to express it. In addition, this algorithm provides only limited diagnostic information. Here we propose a number of alternative solutions. First, we show that the compositional application of SNZ can be weakened: some networks can be guaranteed to be free from Zeno-timelocks, even if not every component is strongly non-zeno. Secondly, we present new syntactic, sufficient-only conditions that complement SNZ. Finally, we describe a sufficient-and-necessary condition that only requires a simple form of reachability analysis. Furthermore, our conditions identify the cause of zeno-timelocks directly on the model, in the form of unsafe loops. We also comment on a tool that we have developed, which implements the syntactic checks on Uppaal models. The tool is also able to derive, from those unsafe loops in a given automaton (in general, an Uppaal model representing a product automaton of a given network), the reachability formulas that characterise the occurrence of zeno-timelocks. A modified version of the carrier sense multiple access with collision detection protocol is used as a case-study.<\/jats:p>","DOI":"10.1007\/s00165-006-0010-7","type":"journal-article","created":{"date-parts":[[2006,9,27]],"date-time":"2006-09-27T12:58:10Z","timestamp":1159361890000},"page":"459-493","source":"Crossref","is-referenced-by-count":21,"title":["How to stop time stopping"],"prefix":"10.1145","volume":"18","author":[{"given":"Howard","family":"Bowman","sequence":"first","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK"}]},{"given":"Rodolfo","family":"G\u00f3mez","sequence":"additional","affiliation":[{"name":"Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK"}]}],"member":"320","reference":[{"issue":"3","key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1016\/S0304-3975(02)00334-1","article-title":"The power of reachability testing for timed automata","volume":"1","author":"Aceto L","year":"2003","journal-title":"Theor Comput Sci"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1024"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_2_4_2","unstructured":"Alur R Madhusudan P (2004) Decision problems for timed automata: a survey. In: Bernardo M Corradini F (eds) Formal methods for the design of real-time systems . International School on Formal Methods for the design of Computer Communication and Software Systems SFM-RT 2004. Revised Lectures Bertinoro Italy 2004 number 3185 in LNCS pp 200\u2013236 Springer Berlin Heidelberg New York"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Berhmann G David A Larsen K (2004) A tutorial on uppaal . In: Bernardo M Corradini F (eds) Formal Methods for the design of real-time systems . International School on Formal Methods for the design of Computer Communication and Software Systems SFM-RT 2004. Revised Lectures LNCS 3185 Springer Berlin Heidelberg New York pp 200\u2013236","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050032"},{"key":"e_1_2_1_2_7_2","volume-title":"Concurrency theory, calculi and automata for modelling untimed and timed concurrent systems","author":"Bowman H","year":"2006"},{"issue":"53","key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1016\/S1567-8326(02)00036-X","article-title":"Automated analysis of an audio control protocol using uppaal","volume":"52","author":"Bengtsson J","year":"2002","journal-title":"J Logic Algebraic Programm"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bowman H Gomez R Su L (2005) A tool for the syntactic detection of zeno-timelocks in timed automata. In: ENTCS 139(1):25\u2013 47 November 2005. Proceedings of the 6th AMAST Workshop on Real-time Systems (ARTS 2004)","DOI":"10.1016\/j.entcs.2005.09.006"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Berhmann G Hune T Vaandrager F (2001) Distributed timed model checking\u2014how the search order matters. In: Proceedings of CAV 2000 number 1855 in LNCS Springer Berlin Heidelberg New York pp 216\u2013231","DOI":"10.1007\/10722167_19"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0920-5489(94)90002-7"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Bowman H (1999) Modelling timeouts without timelocks. In: ARTS\u201999 Formal Methods for Real-Time and Probabilistic Systems 5th International AMAST Workshop LNCS 1601 Springer Berlin Heidelberg New York pp 335\u2013353","DOI":"10.1007\/3-540-48778-6_20"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bowman H (2001) Time and action lock freedom properties for timed automata. In: Kim M Chin B Kang S Lee D (eds) FORTE 2001 Formal Techniques for Networked and Distributed Systems Cheju Island Korea 2001. Kluwer Dordrecht pp 119\u2013134","DOI":"10.1007\/0-306-47003-9_8"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Bornot S Sifakis J (1998) On the composition of hybrid systems. In: Hybrid systems: computation and control LNCS vol 1386 Springer Berlin Heidelberg New York pp 49\u201363","DOI":"10.1007\/3-540-64358-3_31"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Bornot S Sifakis J Tripakis S (1998) Modeling urgency in timed systems. In: Compositionality: the significant difference international symposium COMPOS\u201997 Bad Malente Germany September 8\u201312 1997. Revised Lectures LNCS vol 1536 Springer Berlin Heidelberg New York pp 103\u2013129","DOI":"10.1007\/3-540-49213-5_5"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Bengtsson J Yi W (2004) Timed automata: semantics algorithms and tools. In: Reisig W Rozenberg G (eds) Lecture notes on concurrency and Petri Nets LNCS vol 3098. Springer Berlin Heidelberg New York","DOI":"10.1007\/978-3-540-27755-2_3"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio PR Katoen J-P Ruys TC Tretmans J (1997) The bounded retransmission protocol must be on time! In: Brinksma E (ed) Proceedings of the 3 workshop on tools and algorithms for the construction and analysis of systems Enschede The Netherlands vol 1217 of LNCS Springer Berlin Heidelberg New York pp 416\u2013431","DOI":"10.1007\/BFb0035403"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Daws C Olivero A Tripakis S Yovine S (1996) The tool KRONOS. In: Hybrid systems III Verification and Control LNCS 1066 . Springer Berlin Heidelberg New York","DOI":"10.1007\/BFb0020947"},{"key":"e_1_2_1_2_19_2","unstructured":"Gebremichael B Vaandrager F Zhang M (2006) Analysis of a protocol for dynamic configuration of IPv4 link local addresses using uppaal. Technical Report ICIS-R06XX Radboud University Nijmegen The Netherlands"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Hendriks M Behrmann G Larsen K Niebert P Vaandrager F (2004) Adding symmetry reduction to uppaal. In: Larsen K Niebert P (eds) Proceedings of FORMATS 2003 LNCS 2791 Springer Berlin Heidelberg New York pp 46\u201359","DOI":"10.1007\/978-3-540-40903-8_5"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Henzinger T Ho P-H (1995) HyTech: The Cornell HYbrid TECHnology tool. In: Proceedings of TACAS workshop on tools and algorithms for the construction and analysis of systems","DOI":"10.1007\/3-540-60472-3_14"},{"issue":"1","key":"e_1_2_1_2_22_2","first-page":"43","article-title":"Guided synthesis of control programs using uppaal","volume":"8","author":"Hune T","year":"2001","journal-title":"Nordic J Comput"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Iversen T Kristoffersen K Larsen K Laursen M Madsen R Mortensen S Pettersson P Thomasen C (2000) Model-checking real-time control programs -Verifying LEGO mindstorms systems using uppaal . In: Proceedings of the 12th Euromicro conference on real-time systems pp 147\u2013155","DOI":"10.1109\/EMRTS.2000.854002"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Larsen K Berhmann G Brinksma E Fehnker A Hune T Pettersson P Romijn J (2001) As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In Proceedings of CAV 2001 number 2102 in LNCS Springer Berlin Heidelberg New York pp 493\u2013505","DOI":"10.1007\/3-540-44585-4_47"},{"key":"e_1_2_1_2_26_2","volume-title":"Communication and concurrency","author":"Milner R","year":"1989"},{"key":"e_1_2_1_2_27_2","unstructured":"Regan T (1993) Multimedia in temporal LOTOS: A lip synchronisation algorithm. In: PSTV XIII 13th protocol spec. testing and verification . North-Holland Amsterdam"},{"key":"e_1_2_1_2_28_2","volume-title":"Data and computer communications","author":"Stallings W","year":"2000","edition":"6"},{"key":"e_1_2_1_2_29_2","unstructured":"Tripakis S (1998) The analysis of timed systems in practice. PhD thesis Universite Joseph Fourier Grenoble France December 1998"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Tripakis S (1999) Verifying progress in timed systems. In: ARTS\u201999 formal methods for real-time and probabilistic systems 5th international AMAST workshop LNCS vol 1601. Springer Berlin Heidelberg New York","DOI":"10.1007\/3-540-48778-6_18"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050009"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-006-0010-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-006-0010-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-006-0010-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:43:36Z","timestamp":1641483816000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-006-0010-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,12]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,12]]}},"alternative-id":["10.1007\/s00165-006-0010-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-006-0010-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,12]]}}}