{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T10:09:00Z","timestamp":1762250940309},"reference-count":13,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1984,8,1]],"date-time":"1984-08-01T00:00:00Z","timestamp":460166400000},"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":10577,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Computer and System Sciences"],"published-print":{"date-parts":[[1984,8]]},"DOI":"10.1016\/0022-0000(84)90015-1","type":"journal-article","created":{"date-parts":[[2003,12,4]],"date-time":"2003-12-04T07:01:00Z","timestamp":1070521260000},"page":"80-98","source":"Crossref","is-referenced-by-count":4,"title":["A generalized nexttime operator in temporal logic"],"prefix":"10.1016","volume":"29","author":[{"given":"F.","family":"Kr\u00f6ger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0022-0000(84)90015-1_BIB1","series-title":"Proceedings, Seventh Annual ACM Symposium on Principles of Programming Languages","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/0022-0000(84)90015-1_BIB2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11205-7","article-title":"Verifying concurrent processes using temporal logic","author":"Hailpern","year":"1982"},{"key":"10.1016\/0022-0000(84)90015-1_BIB3","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1109\/TCOM.1983.1095720","article-title":"Modular verification of computer communication protocols","volume":"Com-31","author":"Hailpern","year":"1983","journal-title":"IEEE Trans. Comm."},{"key":"10.1016\/0022-0000(84)90015-1_BIB4","article-title":"Tense Logic and the Theory of Linear Order","author":"Kamp","year":"1968"},{"key":"10.1016\/0022-0000(84)90015-1_BIB5","series-title":"Proceedings 3rd International Symposium on Automata, Languages and Programming","first-page":"87","article-title":"Logical rules of natural reasoning about programs","author":"Kr\u00f6ger","year":"1976"},{"key":"10.1016\/0022-0000(84)90015-1_BIB6","series-title":"Proceedings, IFIP Working Conference on Formal Description of Programming Concepts","first-page":"441","article-title":"A uniform logical basis for the description, specification and verification of programs","author":"Kr\u00f6ger","year":"1978"},{"key":"10.1016\/0022-0000(84)90015-1_BIB7","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF00286493","article-title":"Infinite proof rule for loops","volume":"14","author":"Kr\u00f6ger","year":"1980","journal-title":"Acta Inform."},{"key":"10.1016\/0022-0000(84)90015-1_BIB8","series-title":"Information Processing 80","first-page":"41","article-title":"Logics of programs","author":"Manna","year":"1980"},{"key":"10.1016\/0022-0000(84)90015-1_BIB9","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1145\/357172.357178","article-title":"Proving liveness properties of concurrent programs","volume":"4","author":"Owicki","year":"1982","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/0022-0000(84)90015-1_BIB10","series-title":"Proceedings, 18th Annual Symposium on Foundations of Computer Science","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/0022-0000(84)90015-1_BIB11","series-title":"Proceedings, Symposium on Semantics of Concurrent Computation","first-page":"1","article-title":"The temporal semantics of concurrent computation","author":"Pnueli","year":"1979"},{"key":"10.1016\/0022-0000(84)90015-1_BIB12","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1016\/0304-3975(81)90110-9","article-title":"The temporal semantics of concurrent programs","volume":"13","author":"Pnueli","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0022-0000(84)90015-1_BIB13","doi-asserted-by":"crossref","first-page":"2486","DOI":"10.1109\/TCOM.1982.1095451","article-title":"From state machines to temporal logic: Specification methods for protocol standards","volume":"Com-30","author":"Schwartz","year":"1982","journal-title":"IEEE Trans. Comm."}],"container-title":["Journal of Computer and System Sciences"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0022000084900151?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0022000084900151?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T08:51:31Z","timestamp":1550307091000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0022000084900151"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984,8]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1984,8]]}},"alternative-id":["0022000084900151"],"URL":"https:\/\/doi.org\/10.1016\/0022-0000(84)90015-1","relation":{},"ISSN":["0022-0000"],"issn-type":[{"value":"0022-0000","type":"print"}],"subject":[],"published":{"date-parts":[[1984,8]]}}}