{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T14:07:37Z","timestamp":1648649257015},"reference-count":25,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4156,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1016\/s0304-3975(01)00186-4","type":"journal-article","created":{"date-parts":[[2002,10,15]],"date-time":"2002-10-15T13:27:27Z","timestamp":1034688447000},"page":"347-388","source":"Crossref","is-referenced-by-count":5,"title":["Decidable verification for reducible timed automata specified in a first order logic with time"],"prefix":"10.1016","volume":"275","author":[{"given":"Dani\u00e8le","family":"Beauquier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anatol","family":"Slissenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(01)00186-4_BIB1","series-title":"Workshop on Theory of Hybrid Systems, 1992","first-page":"209","article-title":"Hybrid automata","volume":"vol. 736","author":"Alur","year":"1993"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Alur","year":"1994","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/S0304-3975(01)00186-4_BIB3","doi-asserted-by":"crossref","first-page":"116","DOI":"10.1145\/227595.227602","article-title":"The benefits of relaxing punctuality","volume":"43","author":"Alur","year":"1996","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB4","series-title":"FoSSaCS\u201998: Foundations of Computer Science and Computation Structures","first-page":"81","article-title":"Pumping lemmas for timed automata","volume":"vol. 1378","author":"Beauquier","year":"1998"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB5","unstructured":"D. Beauquier, A. Slissenko, On semantics of algorithms with continuous time, Technical Report 97\u201315, Revised Version, Department of Informatics, 1997, University Paris 12 (available at http:\/\/www.eecs.umich.edu\/gasm\/ and at http:\/\/www.univ-paris12.fr\/lacl\/)."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB6","series-title":"TAPSOFT\u201997: Theory and Practice of Software Development","first-page":"201","article-title":"The railroad crossing problem: towards semantics of timed algorithms and their model-checking in high-level languages","volume":"vol. 1214","author":"Beauquier","year":"1997"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB7","doi-asserted-by":"crossref","unstructured":"D. Beauquier, A. Slissenko, Decidable classes of the verification problem in a timed predicate logic, Proc. 12th Internat. Symp. on Fundamentals of Computation Theory (FCT\u201999), Iasi, Rumania, August 30\u2013September 3, Lecture Notes in Computer Science, vol. 1684, Springer, Berlin, 1999, pp. 100\u2013111.","DOI":"10.1007\/3-540-48321-7_7"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB8","doi-asserted-by":"crossref","unstructured":"D. Beauquier, A. Slissenko, A first order logic for specification of timed algorithms: basic properties and a decidable class, Ann. Pure Appl. Logic. (2001) to appear.","DOI":"10.1016\/S0168-0072(01)00049-5"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB9","series-title":"Logic for Concurrency, Structure versus Automata","first-page":"41","article-title":"Automated temporal reasoning about reactive systems","volume":"vol. 1043","author":"Emerson","year":"1996"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB10","doi-asserted-by":"crossref","unstructured":"A. Emerson, R. Trefler, Parametric quantitative temporal reasoning, Proc. IEEE-CS Conf. on Logic in Computer Science (LICS), 1999, pp. 336\u2013346.","DOI":"10.1109\/LICS.1999.782628"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB11","series-title":"Computer Science Logics, Selected papers from CSL\u201995","first-page":"266","article-title":"The railroad crossing problem","volume":"vol. 1092","author":"Gurevich","year":"1996"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB12","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S0747-7171(88)80006-3","article-title":"Complexity of deciding Tarski algebra","volume":"5","author":"Yu. Grigoriev","year":"1988","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB13","article-title":"Time and Probability in Formal Design of Distributed Systems","volume":"vol. 1","author":"Hansson","year":"1994"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB14","first-page":"439","article-title":"It's about time: real-time logics reviewed","volume":"vol. 1466","author":"Henzinger","year":"1998"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB15","series-title":"Hybrid and Real-Time Systems","first-page":"48","article-title":"From quantity to quality","volume":"vol. 1201","author":"Henzinger","year":"1997"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB16","doi-asserted-by":"crossref","unstructured":"C. Heitmeyer, N. Lynch, The generalized railroad crossing: a case study in formal verification of real-time systems, Proc. Real-Time Systems Symp., San Juan, Puerto Rico, IEEE, 1994.","DOI":"10.1109\/REAL.1994.342724"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB17","unstructured":"C. Heitmeyer, N. Lynch, Formal verification of real-time systems using timed automata, in: C. Heitmeyer, D. Mandrioli (Eds.), Formal Methods for Real-Time Computing, in: B. Krishnamurthy (Ed.), Trends in Software, vol. 5, Wiley, New York, 1996, pp. 83\u2013106."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB18","doi-asserted-by":"crossref","unstructured":"Y. Hirshfeld, A. Rabinovich, A framework for decidable metrical logics, Proc. ICALP\u201999, Lecture Notes in Computer Science, vol. 1644, Springer, Berlin, 1999, pp. 422\u2013432.","DOI":"10.1007\/3-540-48523-6_39"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB19","unstructured":"Y. Hirshfeld, A. Rabinovich, Quantitative temporal logic, Proc. Comput. Sci. Logic (CSL99), Lecture Notes in Computer Science, vol. 1683, Springer, Berlin, 1999, pp. 172\u2013187."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB20","unstructured":"A. Rabinovich, Automata over continuous time, Manuscript, 1998, 32pp."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB21","unstructured":"A. Rabinovich, Expressive completeness of duration calculus, Manuscript, 1998, 33pp."},{"issue":"3","key":"10.1016\/S0304-3975(01)00186-4_BIB22","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1016\/S0747-7171(10)80003-3","article-title":"On the computational complexity and geometry of the first-order theory of the reals, parts 1\u20133","volume":"13","author":"Renegar","year":"1992","journal-title":"J. Symbolic Comput."},{"key":"10.1016\/S0304-3975(01)00186-4_BIB23","series-title":"Software Engineering","author":"Sommerville","year":"1992"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB24","article-title":"Automata and hybrid systems","author":"Trakhtenbrot","year":"1998"},{"key":"10.1016\/S0304-3975(01)00186-4_BIB25","unstructured":"T. Wilke, Automaten und Logiken zur Beschreibung zeitabh\u00e4ngiger Systeme, Ph.D. Thesis, Institut f\u00fcr Informatik und Praktische Mathematik, Christian-Albrechts-Universit\u00e4t zu Kiel, Bericht Nr. 9408, Juli 1994."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001864?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397501001864?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T12:20:15Z","timestamp":1556713215000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397501001864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":25,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["S0304397501001864"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(01)00186-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}