{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,14]],"date-time":"2024-06-14T13:56:22Z","timestamp":1718373382032},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1998,3,1]],"date-time":"1998-03-01T00:00:00Z","timestamp":888710400000},"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":[[1998,3]]},"abstract":"Abstract.<\/jats:title>\n Enhanced Timed-LOTOS, denoted ET-LOTOS, is an extension of LOTOS that allows the modelling of real-time behaviours. It covers all the aspects of full LOTOS, including data types, it supports both a dense and a discrete time domain and can manipulate time values as any other data values. A tutorial on ET-LOTOS, showing many application examples, has already been published [L\u00e9L97]. The present paper adds to it by providing an in-depth presentation of its theoretical aspects. The complete semantics is given and explained, and its properties are studied. In particular, we prove that the semantics is consistent and that strong bisimulation is a congruence. This requires to deal carefully with the presence of negative premises in the operational semantics, which are necessary to express urgency. ET-LOTOS is also shown to be a conservative extension of LOTOS for guarded processes, and is the basis of the timed extension of LOTOS currently developed by ISO [ISO98]. To our knowledge, this is the first in-depth study of a language that combines data types and real-time behaviours.<\/jats:p>","DOI":"10.1007\/s001650050015","type":"journal-article","created":{"date-parts":[[2002,8,25]],"date-time":"2002-08-25T07:30:30Z","timestamp":1030260630000},"page":"248-266","source":"Crossref","is-referenced-by-count":14,"title":["A Formal Definition of Time in LOTOS"],"prefix":"10.1145","volume":"10","author":[{"given":"Luc","family":"L\u00e9onard","sequence":"first","affiliation":[{"name":"University of Li\u00e8ge, Institut Montefiore, Li\u00e8ge, Belgium, BE"}]},{"given":"Guy","family":"Leduc","sequence":"additional","affiliation":[{"name":"University of Li\u00e8ge, Institut Montefiore, Li\u00e8ge, Belgium, BE"}]}],"member":"320","reference":[{"key":"p_1","volume-title":"Real-time CSP, and its relationship to ETLOTOS. Internal report","author":"Bryans J.","year":"1994"},{"key":"p_2","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/200836.200876","article-title":"Bisimulation can\u2019t be traced","volume":"42","author":"Bloom B.","year":"1995","journal-title":"Journal of the ACM"},{"key":"p_3","first-page":"205","volume-title":"Theories and Experiences for Real-Time System Development. Amast Series in Computing","author":"Bolognesi T.","year":"1994"},{"issue":"1","key":"p_4","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0169-7552(87)90085-7","article-title":"Introduction to the ISO Specification Language LOTOS","volume":"14","author":"Bo","year":"1987","journal-title":"Computer Networks and ISDN Systems"},{"key":"p_6","volume-title":"Real-time CSP. In : T","author":"Da","year":"1994"},{"key":"p_7","volume-title":"Hybrid Systems III, Verification and Control, LNCS 1066","author":"Daws C.","year":"1996"},{"key":"p_8","first-page":"332","volume-title":"CONCUR '90","author":"Gro","year":"1990"},{"key":"p_9","volume-title":": Transition system specification with negative premises. Theoretical Computer Science 118","author":"Gro","year":"1993"},{"key":"p_10","first-page":"2","article-title":"Structured Operational Semantics and Bisimulation as a Congruence","volume":"100","author":"Gr","year":"1992","journal-title":"Information and Computation"},{"key":"p_11","volume-title":"A Timed Automaton Model for ET-LOTOS Verification. In : T","author":"Her","year":"1997"},{"key":"p_13","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-60630-0_3","volume-title":"A user guide to HyTech","author":"Henzinger T.","year":"1995"},{"key":"p_14","volume-title":"LOTOS, a Formal Description Technique Based on the Temporal Ordering of Obser~ational Beha~iour. IS","year":"1989"},{"key":"p_15","volume-title":"May 98, 209"},{"key":"p_16","first-page":"215","volume-title":"North-Holland","author":"Led","year":"1986"},{"key":"p_17","first-page":"87","volume-title":"North-Holland","author":"Le","year":"1993"},{"key":"p_18","first-page":"483","volume-title":"North-Holland","author":"Le","year":"1994"},{"issue":"3","key":"p_19","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/S0169-7552(96)00078-5","article-title":"An Introduction to ET-LOTOS for the Description of Time-Sensitive Systems","volume":"29","author":"Le","year":"1997","journal-title":"Computer Networks and ISDN Systems"},{"key":"p_20","volume-title":"Formal Aspects of Computing, (E), 10","author":"Le","year":"1998"},{"key":"p_22","volume-title":"The Tick-Tock case study for the assessment of Timed FDTs. : In A","author":"Le","year":"1994"},{"key":"p_23","volume-title":"Oct.","author":"Larsen K.","year":"1997"},{"key":"p_24","volume-title":"Communication and Concurrency","author":"Mil","year":"1989"},{"key":"p_25","first-page":"401","volume-title":"CONCUR '90","author":"Mo","year":"1990"},{"key":"p_26","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(92)90008-4","article-title":"A Calculus of Mobile Processes - I\\II","volume":"100","author":"Milner R.","year":"1992","journal-title":"Information and Computation"},{"key":"p_27","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1016\/0169-7552(92)90013-G","article-title":"Introduction to the Algebraic Specifications Based on the Language ACT ONE","volume":"23","author":"de Meer J.","year":"1992","journal-title":"Computer Networks and ISDN Systems"},{"key":"p_28","volume-title":"Computer Science Dept.","author":"Plo","year":"1981"},{"key":"p_29","series-title":"Amast Series in Computing","volume-title":"Theories and Experiences for Real-Time System Development","author":"Quemada J.","year":"1994"},{"key":"p_30","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1016\/0304-3975(88)90030-8","volume":"58","author":"Re","year":"1988","journal-title":"Theoretical Computer Science"},{"key":"p_31","volume-title":"B. Mounier, M. Rodr\u0131 guez Artalego, eds., Automata, Languages and Programming, 18, LNCS 510","author":"Wan","year":"1991"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650050015.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650050015\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650050015","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:26:10Z","timestamp":1641482770000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650050015"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,3]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,3]]}},"alternative-id":["10.1007\/s001650050015"],"URL":"https:\/\/doi.org\/10.1007\/s001650050015","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1998,3]]}}}