{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:26Z","timestamp":1761611066970},"reference-count":13,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,25]],"date-time":"2013-07-25T00:00:00Z","timestamp":1374710400000},"content-version":"vor","delay-in-days":4529,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1016\/s0004-3702(01)00059-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T16:57:34Z","timestamp":1027616254000},"page":"137-162","source":"Crossref","is-referenced-by-count":9,"title":["Min-max Computation Tree Logic"],"prefix":"10.1016","volume":"127","author":[{"given":"Pallab","family":"Dasgupta","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"P.P.","family":"Chakrabarti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jatindra Kumar","family":"Deka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"1","key":"10.1016\/S0004-3702(01)00059-5_BIB001","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1006\/inco.1993.1025","article-title":"Real time logics: Complexity and expressiveness","volume":"104","author":"Alur","year":"1993","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/S0004-3702(01)00059-5_BIB002","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1006\/inco.1993.1024","article-title":"Model checking in dense real-time","volume":"104","author":"Alur","year":"1993","journal-title":"Inform. and Comput."},{"issue":"1","key":"10.1016\/S0004-3702(01)00059-5_BIB003","doi-asserted-by":"crossref","first-page":"181","DOI":"10.1145\/174644.174651","article-title":"A really temporal logic","volume":"41","author":"Alur","year":"1994","journal-title":"J. ACM"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB004","doi-asserted-by":"crossref","unstructured":"R. Alur, Timed Automata, Manuscript: www.cis.upenn.edu\/~alur\/Nato97.ps.gz, 1998","DOI":"10.1109\/REAL.1998.739751"},{"issue":"4","key":"10.1016\/S0004-3702(01)00059-5_BIB005","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","article-title":"Symbolic model checking for sequential circuit verification","volume":"13","author":"Burch","year":"1994","journal-title":"IEEE Trans. Computer Aided Design"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB006","series-title":"Theories and Experiences for Real-Time System Development","article-title":"Real-time symbolic model checking for discrete time models","author":"Campos","year":"1994"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB007","series-title":"Workshop on Languages, Compilers and Tools for Real-Time Systems","article-title":"Verus: A tool for quantitative analysis of finite-state real-time systems","author":"Campos","year":"1995"},{"issue":"2","key":"10.1016\/S0004-3702(01)00059-5_BIB008","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","article-title":"Automatic verification of finite-state concurrent systems using temporal logic specifications","volume":"8","author":"Clarke","year":"1986","journal-title":"ACM Trans. Program. Lang. Systems"},{"issue":"6","key":"10.1016\/S0004-3702(01)00059-5_BIB009","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1109\/6.499951","article-title":"Computer aided verification","volume":"33","author":"Clarke","year":"1996","journal-title":"IEEE Spectrum"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB010","series-title":"Introduction to Algorithms","author":"Cormen","year":"1990"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB011","series-title":"First Annual Workshop on Computer-Aided Verification, France","article-title":"Quantitative temporal reasoning","author":"Emerson","year":"1989"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB012","series-title":"Proc. ED&TC","first-page":"182","article-title":"Using MTBDDs for discrete timed symbolic model checking","author":"Kropf","year":"1997"},{"key":"10.1016\/S0004-3702(01)00059-5_BIB013","series-title":"Computational Complexity","author":"Papadimitriou","year":"1994"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370201000595?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370201000595?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,25]],"date-time":"2019-04-25T12:28:40Z","timestamp":1556195320000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370201000595"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["S0004370201000595"],"URL":"https:\/\/doi.org\/10.1016\/s0004-3702(01)00059-5","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}