{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,24]],"date-time":"2025-02-24T05:12:21Z","timestamp":1740373941632,"version":"3.37.3"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2010,7,23]],"date-time":"2010-07-23T00:00:00Z","timestamp":1279843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2010,9]]},"DOI":"10.1007\/s00236-010-0121-8","type":"journal-article","created":{"date-parts":[[2010,7,22]],"date-time":"2010-07-22T04:14:53Z","timestamp":1279772093000},"page":"279-311","source":"Crossref","is-referenced-by-count":6,"title":["Reachability results for timed automata with unbounded data structures"],"prefix":"10.1007","volume":"47","author":[{"given":"Ruggero","family":"Lanotte","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Maggiolo-Schettini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Troina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,7,23]]},"reference":[{"key":"121_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The Spi calculus. In: 4th ACM Conference on Computer and Communications Security, pp. 36\u201347. ACM Press (1997)","DOI":"10.1145\/266420.266432"},{"key":"121_CR2","doi-asserted-by":"crossref","unstructured":"Abdullah, P.A., Jonsson, B.: Verifying networks of timed processes. In: Proceedings of TACAS\u2019 98, of LNCS, vol. 1384, pp. 298\u2013312. Springer (1998)","DOI":"10.1007\/BFb0054179"},{"issue":"2","key":"121_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"121_CR4","first-page":"200","volume":"3185","author":"G. Behrmann","year":"2004","unstructured":"Behrmann G., David A., Larsen K.G.: A tutorial on uppaal. Springer LNCS 3185, 200\u2013236 (2004)","journal-title":"Springer LNCS"},{"issue":"3","key":"121_CR5","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1109\/32.75415","volume":"17","author":"B. Berthomieu","year":"1991","unstructured":"Berthomieu B., Diaz M.: Modeling and verification of time dependent systems using time petri nets. IEEE Trans. Softw. Eng. 17(3), 259\u2013273 (1991)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"121_CR6","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Echahed, R., Robbana, R.: On the automatic verification of systems with continuous variables and unbounded discrete data structures. In: Proceedings Hybrid System II, Springer LNCS, vol. 999, pp. 64\u201385 (1995)","DOI":"10.1007\/3-540-60472-3_4"},{"key":"121_CR7","doi-asserted-by":"crossref","unstructured":"Burrows, M., Abadi, M., Needham, R.: A logic for authentication. Technical Report 39, Digital Systems Research Center, Feb (1989)","DOI":"10.1145\/74850.74852"},{"key":"121_CR8","unstructured":"Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed analysis of security protocols. Journal of Computer Security. A preliminary report appeared as CTIT Technichal Report TR\u2013CTIT\u201305\u201314, University of Twente, The Netherlands (2005) (to appear)"},{"key":"121_CR9","unstructured":"Cremers, C.J.F., Mauw, S., de Vink, E.P.: Defining authentication in a trace model. In: 1st International Workshop on Formal Aspects in Security and Trust (Fast 2003), pp. 131\u2013145, Pisa, IITT-CNR technical report (2003)"},{"key":"121_CR10","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1016\/S0304-3975(02)00743-0","volume":"302","author":"Z. Dang","year":"2003","unstructured":"Dang Z.: Pushdown time automata: a binary reachability characterization and safety verification. Theor. Comp. Sci. 302, 93\u2013121 (2003)","journal-title":"Theor. Comp. Sci."},{"issue":"2","key":"121_CR11","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D. Dolev","year":"1983","unstructured":"Dolev D., Yao A.C.-C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013207 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"121_CR12","doi-asserted-by":"crossref","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Non interference for the analysis of cryptographic protocols. In: International Conference on Automata, Languages and Programming (ICALP\u201900) of LNCS, vol. 1853, pp. 354\u2013372. Springer (2000)","DOI":"10.1007\/3-540-45022-X_31"},{"issue":"4","key":"121_CR13","first-page":"301","volume":"9","author":"J. Hoenicke","year":"2002","unstructured":"Hoenicke J., Olderog E.R.: CSP-OZ-DC: a combination of specification techniques for processes, data and time. Nord. J. Comput. 9(4), 301\u2013334 (2002)","journal-title":"Nord. J. Comput."},{"key":"121_CR14","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1016\/S0304-3975(01)00269-9","volume":"289","author":"O.H. Ibarra","year":"2002","unstructured":"Ibarra O.H., Su J.: Augmenting the discrete timed automaton with other data structures. Theor. Comput. Sci. 289, 191\u2013204 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"121_CR15","doi-asserted-by":"crossref","unstructured":"Kosaraju, S.R.: Decidability of reachability in vector addition systems. In: 14th Annual ACM Symposium on Theory of Computing, pp. 267\u2013281. ACM Press (1982)","DOI":"10.1145\/800070.802201"},{"key":"121_CR16","doi-asserted-by":"crossref","unstructured":"Krcal, P., Yi, W.: Communicating Timed Automata: The More Synchronous, the More Difficult to Verify. CAV\u201906 of LNCS, vol. 4144, pp. 249\u2013262, Springer (2006)","DOI":"10.1007\/11817963_24"},{"key":"121_CR17","unstructured":"Lanotte, R.: Expressive power of hybrid systems with real variables, integer variables and arrays. J of Automata, Languages and Combinatorics, (accepted for publication)"},{"key":"121_CR18","doi-asserted-by":"crossref","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Timed automata with data structures for distributed systems design and analysis. In: 3nd International Conference on Software Engineering and Formal Methods (SEFM\u201905), pp. 44\u201353. IEEE Computer Society Press (2005)","DOI":"10.1109\/SEFM.2005.49"},{"key":"121_CR19","doi-asserted-by":"crossref","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: 10th International Computer Security Foundations Workshop (CSFW\u201997), pp. 31\u201344. IEEE Computer Society Press (1997)","DOI":"10.1109\/CSFW.1997.596782"},{"key":"121_CR20","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1016\/j.entcs.2004.02.009","volume":"99","author":"M. Napoli","year":"2004","unstructured":"Napoli M., Parente M., Peron A.: Specification and verification of protocols with time constraints. Electronic Notes Theor. Comput. Sci. 99, 205\u2013227 (2004)","journal-title":"Electronic Notes Theor. Comput. Sci."},{"issue":"3","key":"121_CR21","doi-asserted-by":"crossref","first-page":"197","DOI":"10.3233\/JCS-2001-9302","volume":"9","author":"L.C. Paulson","year":"2001","unstructured":"Paulson L.C.: Relations between secrets: two formal analyses of the Yahalom protocol. J. Comput. Secur. 9(3), 197\u2013216 (2001)","journal-title":"J. Comput. Secur."},{"key":"121_CR22","unstructured":"The Object-Z specification language. Kluwer Academic Publishers, Norwell (1999)"},{"key":"121_CR23","doi-asserted-by":"crossref","unstructured":"Valero Ruiz, V., Cuartero Gomez, F., de Frutos-Escrig, D.: On non-decidability of reachability for timed-arc Petri nets. In: Proceedings 8th International Work. Petri Nets and Performance Models (PNPM\u201903) IEEE Computer Society Press, pp. 188\u2013196 (1999)","DOI":"10.1109\/PNPM.1999.796565"},{"key":"121_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5537-7","volume-title":"Timed Petri Nets: Theory and Application","author":"J. Wang","year":"1998","unstructured":"Wang J.: Timed Petri Nets: Theory and Application. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"121_CR25","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine S.: Kronos: a verification tool for real-time systems. Int. J. Softw. Tools Technol. Transf. 1, 123\u2013133 (1997)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"5","key":"121_CR26","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C. Zhou","year":"1991","unstructured":"Zhou C., Hoare C.A.R., Ravn A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-010-0121-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-010-0121-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-010-0121-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T06:16:39Z","timestamp":1740291399000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-010-0121-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7,23]]},"references-count":26,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["121"],"URL":"https:\/\/doi.org\/10.1007\/s00236-010-0121-8","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2010,7,23]]}}}