{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T11:17:00Z","timestamp":1768562220971,"version":"3.49.0"},"reference-count":33,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1983,1,1]],"date-time":"1983-01-01T00:00:00Z","timestamp":410227200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1983,1,1]],"date-time":"1983-01-01T00:00:00Z","timestamp":410227200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":11155,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["3KXWlO707"],"award-info":[{"award-number":["3KXWlO707"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["MCSW2 1023"],"award-info":[{"award-number":["MCSW2 1023"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["WO1-b80COh47"],"award-info":[{"award-number":["WO1-b80COh47"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1983]]},"DOI":"10.1016\/0304-3975(83)90097-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T23:48:55Z","timestamp":1027640935000},"page":"127-165","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":38,"title":["The propositional dynamic logic of deterministic, well-structured programs"],"prefix":"10.1016","volume":"27","author":[{"given":"Joseph Y.","family":"Halpern","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John H.","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(83)90097-X_BIB1_1","first-page":"249","article-title":"Finite models of deterministic propositional dynamic logic","author":"Ben-Ari","year":"1981","journal-title":"Proc. 8th Internat. Conf. on Automata, Languages, and Programming"},{"issue":"3","key":"10.1016\/0304-3975(83)90097-X_BIB1_2","doi-asserted-by":"crossref","first-page":"402","DOI":"10.1016\/0022-0000(82)90018-6","article-title":"Deterministic propositional dynamic logic: Finite models, complexity, and completeness","volume":"25","author":"Ben-Ari","year":"1982","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(83)90097-X_BIB2","series-title":"TR78-11-01","article-title":"Expressiveness hierarchy for PDL with rich test","author":"Berman","year":"1978"},{"key":"10.1016\/0304-3975(83)90097-X_BIB3","series-title":"TR77-10-02","article-title":"Test-free propositional dynamic logic is strictly weaker than PDL","author":"Berman","year":"1978"},{"key":"10.1016\/0304-3975(83)90097-X_BIB4","first-page":"48","article-title":"On the expressive power of nondeterminism in dynamic logic","author":"Berman","year":"1982","journal-title":"Proc. 9th Internat. Conf. on Automata, Languages, and Programming"},{"key":"10.1016\/0304-3975(83)90097-X_BIB5","author":"Chlebus","year":"1981","journal-title":"On the computational complexity of satisfiability in propositional logics of programs"},{"key":"10.1016\/0304-3975(83)90097-X_BIB6","author":"Chlebus","year":"1982","journal-title":"Private communication"},{"key":"10.1016\/0304-3975(83)90097-X_BIB7_1","series-title":"Proc. 9th Ann. ACM Symp. on Theory of Computing","first-page":"286","article-title":"Propositional modal logic of programs","author":"Fischer","year":"1977"},{"issue":"2","key":"10.1016\/0304-3975(83)90097-X_BIB7_2","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","article-title":"Propositional dynamic logic of regular programs","volume":"18","author":"Fischer","year":"1979","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(83)90097-X_BIB8","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980","journal-title":"Proc. 7th Ann. Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(83)90097-X_BIB9","article-title":"Theory of Program Structures: Schemes, Semantics, Verification","volume":"36","author":"Greibach","year":"1975"},{"key":"10.1016\/0304-3975(83)90097-X_BIB10","article-title":"On the expressive power of dynamic logic, Part II","author":"Halpern","year":"1981","journal-title":"MIT\/LCS\/TM-204"},{"key":"10.1016\/0304-3975(83)90097-X_BIB11","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1109\/SFCS.1981.49","article-title":"The propositional dynamic logic of deterministic, well-structured programs","author":"Halpern","year":"1981","journal-title":"Proc. 22nd Ann. Symp. on the Foundations of Computer Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB12","article-title":"Logics of programs: Axiomatics and descriptive power","author":"Harel","year":"1978","journal-title":"MIT\/LCS\/TR-200"},{"key":"10.1016\/0304-3975(83)90097-X_BIB13","doi-asserted-by":"crossref","first-page":"310","DOI":"10.1109\/SFCS.1981.38","article-title":"Propositional dynamic logic of context-free programs","author":"Harel","year":"1981","journal-title":"22nd Symp. of the Foundations of Computer Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB14","series-title":"Introduction to Automata Theory, Languages, and Computation","author":"Hoperoft","year":"1979"},{"issue":"1","key":"10.1016\/0304-3975(83)90097-X_BIB15","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1016\/0304-3975(81)90019-0","article-title":"An elementary proof of the completeness of PDL","volume":"14","author":"Kozen","year":"1981","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(83)90097-X_BIB16","series-title":"Proc. IBM Conf.on Logics of Programs","article-title":"A note on equivalences among logics of programs","volume":"131","author":"Meyer","year":"1982"},{"issue":"3","key":"10.1016\/0304-3975(83)90097-X_BIB17","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1016\/0304-3975(82)90071-8","article-title":"Expressing program looping in regular dynamic logic","volume":"18","author":"Meyer","year":"1982","journal-title":"Theoret. Comput. Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB18","first-page":"421","article-title":"On formalized systems of algorithmic logic","volume":"22","author":"Mirkowska","year":"1974","journal-title":"Bull. Acad. Pol. Sci. Ser. Sci. Math. Astr. Phys."},{"key":"10.1016\/0304-3975(83)90097-X_BIB19","first-page":"186","article-title":"Propositional logics of programs: Systems, models, and complexity","author":"Parikh","year":"1980","journal-title":"7th Ann. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(83)90097-X_BIB20","author":"Passy","year":"1982","journal-title":"Filtration lemma for deterministic programming algebras"},{"key":"10.1016\/0304-3975(83)90097-X_BIB21","series-title":"TR47","article-title":"The power of tests in propositional dynamic logic","author":"Peterson","year":"1978"},{"key":"10.1016\/0304-3975(83)90097-X_BIB22","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977","journal-title":"18th IEEE Symp. on the Foundations of Computer Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB23","first-page":"109","article-title":"Semantical considerations of Floyd-Hoare logic","author":"Pratt","year":"1976","journal-title":"17th IEEE Symp. on the Foundations of Computer Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB24_1","first-page":"326","article-title":"A practical decision method for propositional dynamic logic","author":"Pratt","year":"1978","journal-title":"10th Ann. ACM Symp. on the Theory of Computation"},{"issue":"2","key":"10.1016\/0304-3975(83)90097-X_BIB24_2","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0022-0000(80)90061-6","article-title":"A near optimal method for reasoning about action","volume":"20","author":"Pratt","year":"1980","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0304-3975(83)90097-X_BIB25","first-page":"115","article-title":"Models of program logics","author":"Pratt","year":"1979","journal-title":"20th IEEE Symp. on the Foundations of Computer Science"},{"key":"10.1016\/0304-3975(83)90097-X_BIB26","series-title":"Proc. IBM Conf. on Logics of Programs","first-page":"357","article-title":"Using graphs to understand PDL","volume":"131","author":"Pratt","year":"1982"},{"issue":"5","key":"10.1016\/0304-3975(83)90097-X_BIB27","first-page":"227","article-title":"Formalized algorithmic languages","volume":"18","author":"Salwicki","year":"1970","journal-title":"Bull. Acad. Pol. Sci. Ser. Math. Astr. Phys."},{"issue":"2","key":"10.1016\/0304-3975(83)90097-X_BIB28","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationships between nondeterministic and deterministic tape complexities","volume":"4","author":"Savitch","year":"1970","journal-title":"J. Comput. Systems Sci."},{"key":"10.1016\/0304-3975(83)90097-X_BIB29","first-page":"159","article-title":"The complexity of propositional linear temporal logics","author":"Sistla","year":"1982","journal-title":"14th Ann. ACM Symp. in the Theory of Computation"},{"key":"10.1016\/0304-3975(83)90097-X_BIB30","doi-asserted-by":"crossref","first-page":"340","DOI":"10.1109\/SFCS.1981.44","article-title":"Temporal logic can be more expressive","author":"Wolper","year":"1981","journal-title":"22nd IEEE Symp. of the Foundations of Computer Science"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439758390097X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439758390097X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,10]],"date-time":"2025-09-10T04:18:20Z","timestamp":1757477900000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439758390097X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1983]]},"references-count":33,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1983]]}},"alternative-id":["030439758390097X"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(83)90097-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1983]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The propositional dynamic logic of deterministic, well-structured programs","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/0304-3975(83)90097-X","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1983 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}