{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T00:05:51Z","timestamp":1778198751224,"version":"3.51.4"},"reference-count":37,"publisher":"Elsevier BV","issue":"1-3","license":[{"start":{"date-parts":[[2001,12,1]],"date-time":"2001-12-01T00:00:00Z","timestamp":1007164800000},"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":4246,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Pure and Applied Logic"],"published-print":{"date-parts":[[2001,12]]},"DOI":"10.1016\/s0168-0072(01)00049-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T09:36:39Z","timestamp":1027589799000},"page":"13-52","source":"Crossref","is-referenced-by-count":9,"title":["A first order logic for specification of timed algorithms: basic properties and a decidable class"],"prefix":"10.1016","volume":"113","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\/S0168-0072(01)00049-5_BIB1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","article-title":"The algorithmic analysis of hybrid systems","volume":"138","author":"Alur","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB2","first-page":"209","article-title":"Hybrid automata","volume":"vol. 736","author":"Alur","year":"1993"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB3","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."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB4","unstructured":"D. Beauquier, A. Slissenko, On semantics of algorithms with continuous time, Technical Report 97-15, 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\/S0168-0072(01)00049-5_BIB5","first-page":"201","article-title":"The railroad crossing problem","volume":"vol. 1214","author":"Beauquier","year":"1997"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB6","unstructured":"D. Beauquier, A. Slissenko, Decidable verification for reducible timed automata specified in a first order logic with time, Technical Report 98-16, Department of Informatics, University Paris 12, 1998, Available at http:\/\/www.univ-paris12.fr\/lacl\/, submitted for publication."},{"key":"10.1016\/S0168-0072(01)00049-5_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), Ia\u015fi, 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"},{"issue":"5","key":"10.1016\/S0168-0072(01)00049-5_BIB8","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","article-title":"A calculus of duration","volume":"40","author":"Chaochen","year":"1991","journal-title":"Inform. Process. Lett."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB9","series-title":"Handbook of Theoretical Computer Science, vol. B: Formal Models and Sematics","first-page":"995","article-title":"Temporal and modal logic","author":"Emerson","year":"1990"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB10","series-title":"Logic for Concurrency, Structure versus Automata","first-page":"41","article-title":"Automated temporal reasoning about reactive systems","author":"Emerson","year":"1996"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB11","doi-asserted-by":"crossref","unstructured":"Y. Gurevich, J. Huggins, The railroad crossing problem: an experiment with instantaneous actions and immediate reactions, in: H.K. Buening (Ed.), Computer Science Logics, Selected papers from CSL\u201995, Lecture Notes in Computer Science, vol. 1092, Springer, Berlin, pp. 266\u2013290.","DOI":"10.1007\/3-540-61377-3_43"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB12","series-title":"Specification and Validation Methods","first-page":"9","article-title":"Evolving algebra 1993: Lipari guide","author":"Gurevich","year":"1995"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB13","unstructured":"H.A. Hansson, Time and Probability in Formal Design of Distributed Systems, Elsevier, Amsterdam, 1994. (In: H. Zedan (Series Editor), Series: Real Time Safety Critical System, vol. 1.)"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB14","doi-asserted-by":"crossref","unstructured":"T. Henzinger, It's about time: real-time logics reviewed, Proc. 10th CONCUR, Lecture Notes in Computer Science, vol. 1466, Springer, Berlin, 1998, pp. 439\u2013454.","DOI":"10.1007\/BFb0055640"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB15","series-title":"The generalized railroad crossing: a case study in formal verification of real-time systems, Proc. Real-Time Systems Symp., San Juan, Puerto Rico","author":"Heitmeyer","year":"1994"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB16","series-title":"Formal Methods for Real-Time Computing","first-page":"83","article-title":"Formal verification of real-time systems using timed automata","author":"Heitmeyer","year":"1996"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB17","unstructured":"C. Heitmeyer, D. Mandrioli (Eds.), Formal Methods for Real-Time Computing, Wiley, New York, 1996. (In: B. Krishnamurthy (Series Editor), Series: Trends in Software, vol. 5.)."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB18","first-page":"422","volume":"vol. 1644","author":"Hirshfeld","year":"1999"},{"issue":"8","key":"10.1016\/S0168-0072(01)00049-5_BIB19","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1145\/361082.361093","article-title":"A new solution of Dijkstra's concurrent programming problem","volume":"17","author":"Lamport","year":"1974","journal-title":"Comm. ACM"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB20","doi-asserted-by":"crossref","unstructured":"N. Lynch, R. Segala, F. Vaandrager, H. Weinberg, Hybrid i\/o aotomata, Proc. DIMACS\/SYCON Workshop on Verification and Control of Hybrid Systems (Hybrid Systems III: Verification and Control), New Brunswick, NJ, October 1995, Lecture Notes in Computer Science, vol. 1066, Springer, Berlin, 1996, pp. 496\u2013510.","DOI":"10.1007\/BFb0020971"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB21","series-title":"Handbook of Theoretical Computer Science. Vol. B: Formal Models and Sematics","first-page":"1201","article-title":"Operational and algebraic semantics of concurrent processes","author":"Milner","year":"1990"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB22","series-title":"Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"issue":"2","key":"10.1016\/S0168-0072(01)00049-5_BIB23","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","article-title":"Formal verification for fault-tolerant architectures","volume":"21","author":"Owre","year":"1995","journal-title":"IEEE Trans. Software Eng."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB24","series-title":"The temporal logic of programs, Proc. IEEE 18th Annu. Symp. on Foundations in Computer Science","first-page":"46","author":"Pnueli","year":"1977"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB25","unstructured":"PVS, WWW site of PVS papers. http:\/\/www.csl.sri.com\/sri-csl-fm.html."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB26","unstructured":"A. Rabinovich, Decidability in monadic logic of order over finitely variable signals. Manuscript, 1997, 15pp."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB27","unstructured":"A. Rabinovich, Automata over continuous time, Manuscript, 1998, 32pp."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB28","doi-asserted-by":"crossref","first-page":"320","DOI":"10.1006\/inco.1999.2816","article-title":"Expressive completeness of duration calculus","volume":"156","author":"Rabinovich","year":"2000","journal-title":"J. Inform. and Comput."},{"issue":"5","key":"10.1016\/S0168-0072(01)00049-5_BIB29","doi-asserted-by":"crossref","first-page":"669","DOI":"10.1093\/logcom\/8.5.669","article-title":"On the decidability of continuous time specification formalisms","volume":"8","author":"Rabinovich","year":"1998","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB30","unstructured":"A. Rabinovich, Composition theorems for generalized sums, Manuscript, 1999, 20pp."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB31","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/0020-0255(91)90089-D","article-title":"On measures of information quality of knowledge processing systems","volume":"57\u201358","author":"Slissenko","year":"1991","journal-title":"Inform. Sci."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB32","unstructured":"A. Slissenko, Minimizing entropy of knowledge representaion, Proc. 2nd Internat. Conf. on Computer Science and Information Technologies, August 17\u201322, 1999, Yerevan, Armenia, National Academy of Sciences of Armenia, 1999, pp. 2\u20136."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB33","series-title":"Software Engineering","author":"Sommerville","year":"1992"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB34","unstructured":"V.V. Tarasov, Inference search control in expert systems based on explicit meta-rules of inference search, Ph.D. Thesis, St. Petersburg Institute for Informatics and automation, Russian Academy of Sciences, 1996 (in Russian)."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB35","unstructured":"B. Trakhtenbrot, Automata and hybrid systems, in: F. Moller, B. Trakhtenbrot (Eds.), Lecture Notes 153, Computing Science Department, Uppsala University, 1998."},{"key":"10.1016\/S0168-0072(01)00049-5_BIB36","doi-asserted-by":"crossref","unstructured":"M. Vardi, An automata-theoretic approach to linear temporal logic, in: F. Moller, G. Birtwistle (Eds.), Logic for Concurrency. Structure versus Automata, pp. 238\u2013266. Springer-Verlag, 1996. Series: \u201cLecture notes in Computer Science (Tutorial)\u201d, vol. 1043.","DOI":"10.1007\/3-540-60915-6_6"},{"key":"10.1016\/S0168-0072(01)00049-5_BIB37","unstructured":"V. Weispfenning, Mixed real-integer linear quantifier elimination, Proc. 1999 Internat. Symp. on Symbolic and Algebraic Computations (ISSAC\u201999), July 29\u201331, 1999, Vancouver, BC, Canada, ACM Press, New York, 1999, pp. 129\u2013136."}],"container-title":["Annals of Pure and Applied Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007201000495?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0168007201000495?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T04:25:52Z","timestamp":1556511952000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0168007201000495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,12]]},"references-count":37,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2001,12]]}},"alternative-id":["S0168007201000495"],"URL":"https:\/\/doi.org\/10.1016\/s0168-0072(01)00049-5","relation":{},"ISSN":["0168-0072"],"issn-type":[{"value":"0168-0072","type":"print"}],"subject":[],"published":{"date-parts":[[2001,12]]}}}