{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,14]],"date-time":"2026-04-14T18:38:46Z","timestamp":1776191926810,"version":"3.50.1"},"reference-count":86,"publisher":"Elsevier","isbn-type":[{"value":"9780444516909","type":"print"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1016\/s1570-2464(07)80020-6","type":"book-chapter","created":{"date-parts":[[2007,10,4]],"date-time":"2007-10-04T09:38:50Z","timestamp":1191490730000},"page":"971-989","source":"Crossref","is-referenced-by-count":9,"title":["17 Automata-theoretic techniques for temporal reasoning"],"prefix":"10.1016","member":"78","reference":[{"key":"10.1016\/S1570-2464(07)80020-6_bib1","series-title":"Proc. 9th International Conference on Tools and algorithms for the construction and analysis of systems","first-page":"65","article-title":"Resets vs. aborts in linear temporal logic","author":"Armoni","year":"2003"},{"key":"10.1016\/S1570-2464(07)80020-6_bib2","series-title":"Proc. 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"211","article-title":"The ForSpec temporal logic: A new temporal property-specification logic","author":"Armoni","year":"2002"},{"key":"10.1016\/S1570-2464(07)80020-6_bib3","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","article-title":"The temporal logic of branching time","volume":"20","author":"Ben-Ari","year":"1983","journal-title":"Acta Informatica"},{"issue":"8","key":"10.1016\/S1570-2464(07)80020-6_bib4","doi-asserted-by":"crossref","DOI":"10.1109\/TC.1986.1676819","article-title":"Graph-based algorithms for boolean-function manipulation","volume":"C-35","author":"Bryant","year":"1986","journal-title":"IEEE Trans, on Computers"},{"key":"10.1016\/S1570-2464(07)80020-6_bib5","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/0304-3975(80)90069-9","article-title":"Finite automata and sequential networks","volume":"10","author":"Brzozowski","year":"1980","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib6","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1002\/malq.19600060105","article-title":"Weak second-order arithmetic and finite automata","volume":"6","author":"B\u00fcchi","year":"1960","journal-title":"Zeit. Math. Logik und Grundl. Math."},{"key":"10.1016\/S1570-2464(07)80020-6_bib7","series-title":"Proc. International Congress on Logic, Method, and Philosophy of Science. 1960","first-page":"1","article-title":"On a decision method in restricted second order arithmetic","author":"B\u00fcchi","year":"1962"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib8","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","article-title":"Symbolic model checking: 1020 states and beyond","volume":"98","author":"Burch","year":"1992","journal-title":"Information and Computation"},{"key":"10.1016\/S1570-2464(07)80020-6_bib9","doi-asserted-by":"crossref","first-page":"566","DOI":"10.2307\/2273296","article-title":"Logic and time","volume":"44","author":"Burgess","year":"1979","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80020-6_bib10","series-title":"Proc. 13th Advanced Research Working Conference on Correct Hardware Design and Verification Methods","first-page":"191","article-title":"Regular vacuity","author":"Bustan","year":"2005"},{"issue":"1","key":"10.1016\/S1570-2464(07)80020-6_bib11","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/322234.322243","article-title":"Alternation","volume":"28","author":"Chandra","year":"1981","journal-title":"Journal of the Association for Computing Machinery"},{"key":"10.1016\/S1570-2464(07)80020-6_bib12","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0022-0000(74)80051-6","article-title":"Theories of automata on \u03c9-tapes: A simplified approach","volume":"8","author":"Choueka","year":"1974","journal-title":"Journal of Computer and System Sciences"},{"key":"10.1016\/S1570-2464(07)80020-6_bib13","series-title":"Proc. Workshop on Linear Time, Branching Time, and Partial Order in Logics and Models for Concurrency","first-page":"428","article-title":"Expressibility results for linear-time and branching-time logics","author":"Clarke","year":"1988"},{"key":"10.1016\/S1570-2464(07)80020-6_bib14","series-title":"Proc. Workshop on Logic of Programs","first-page":"428","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"Clarke","year":"1988"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib15","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 Transactions on Programming Languages and Systems"},{"key":"10.1016\/S1570-2464(07)80020-6_bib16","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1570-2464(07)80020-6_bib17","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","article-title":"A linear-time model-checking algorithm for the alternation-free modal \u03bc-calculus","volume":"2","author":"Cleaveland","year":"1993","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1570-2464(07)80020-6_bib18","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","article-title":"Memory efficient algorithms for the verification of temporal properties","volume":"1","author":"Courcoubetis","year":"1992","journal-title":"Formal Methods in System Design"},{"key":"10.1016\/S1570-2464(07)80020-6_bib19","first-page":"819","article-title":"Decidability of the weak second-order theory of two successors","volume":"12","author":"Doner","year":"1965","journal-title":"Notices Amer. Math. Soc"},{"key":"10.1016\/S1570-2464(07)80020-6_bib20","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1090\/S0002-9947-1961-0139530-9","article-title":"Decision problems of finite-automata design and related arithmetics","volume":"98","author":"Elgot","year":"1961","journal-title":"Trans. Amer. Math. Soc"},{"key":"10.1016\/S1570-2464(07)80020-6_bib21","series-title":"Proc. Workshop on Logic of Programs","first-page":"79","article-title":"Automata, tableaux, and temporal logics","author":"Emerson","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib22","first-page":"997","article-title":"Temporal and modal logic","volume":"volume B","author":"Emerson","year":"1990"},{"key":"10.1016\/S1570-2464(07)80020-6_bib23","series-title":"Proc. 1th InternationalColloq. on Automata, Languages and Programming","first-page":"169","article-title":"Characterizing correctness properties of parallel programs using fixpoints","author":"Emerson","year":"1980"},{"key":"10.1016\/S1570-2464(07)80020-6_bib24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","article-title":"Decision procedures and expressiveness in the temporal logic of branching time","volume":"30","author":"Emerson","year":"1985","journal-title":"Journal of Computer and System Sciences"},{"issue":"1","key":"10.1016\/S1570-2464(07)80020-6_bib25","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","article-title":"Sometimes and not never revisited: On branching versus linear time","volume":"33","author":"Emerson","year":"1986","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1570-2464(07)80020-6_bib26","series-title":"Proc. 29th IEEE Symp. on Foundations of Computer Science","first-page":"328","article-title":"The complexity of tree automata and logics of programs","author":"Emerson","year":"1988"},{"key":"10.1016\/S1570-2464(07)80020-6_bib27","series-title":"Proc. 32nd IEEE Symp. on Foundations of Computer Science","first-page":"368","article-title":"Tree automata, \u03bc-calculus and determinacy","author":"Emerson","year":"1991"},{"key":"10.1016\/S1570-2464(07)80020-6_bib28","series-title":"Proc. 20th ACM Symp. on Principles of Programming Languages","first-page":"84","article-title":"Modalities for model checking: Branching time logic strikes back","author":"Emerson","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib29","series-title":"Proc. 18th Hawaii International Conference on System Sciences","article-title":"Temporal model checking under generalized fairness constraints","author":"Emerson","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib30","series-title":"Proc. 16th ACM Symp. on Theory of Computing","first-page":"14","article-title":"Deciding branching time logic","author":"Emerson","year":"1984"},{"key":"10.1016\/S1570-2464(07)80020-6_bib31","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":"Journal of Computer and Systems Sciences"},{"key":"10.1016\/S1570-2464(07)80020-6_bib32","series-title":"Proc. 12th Int'l Conf. on Logic for Programming, Artificial Intelligence, and Reasoning","first-page":"728","article-title":"Concepts of automata construction from LTL","author":"Fritz","year":"2005"},{"key":"10.1016\/S1570-2464(07)80020-6_bib33","doi-asserted-by":"crossref","first-page":"135","DOI":"10.2307\/2272556","article-title":"Applications of trees to intermediate logics i","volume":"37","author":"Gabbay","year":"1972","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S1570-2464(07)80020-6_bib34","series-title":"Protocol Specification, Testing, and Verification","first-page":"3","article-title":"Simple on-the-fly automatic verification of linear temporal logic","author":"Gerth","year":"1995"},{"key":"10.1016\/S1570-2464(07)80020-6_bib35","series-title":"Proc. 14th International Coll. on Automata, Languages, and Programming","first-page":"269","article-title":"Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree","author":"Hafer","year":"1987"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib36","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","article-title":"An improved protocol reachability analysis technique","volume":"18","author":"Holzmann","year":"1988","journal-title":"Software Practice and Experi- ence"},{"key":"10.1016\/S1570-2464(07)80020-6_bib37","series-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann","year":"2003"},{"key":"10.1016\/S1570-2464(07)80020-6_bib38","article-title":"Tense Logic and the Theory of Order","author":"Kamp","year":"1968"},{"key":"10.1016\/S1570-2464(07)80020-6_bib39","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","article-title":"Results on the propositional \u03bc-calculus","volume":"27","author":"Kozen","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib40","series-title":"Proceedings of the Conference on Automated Deduction","first-page":"423","article-title":"The complexity of the graded \u03bc-calculus","author":"Kupferman","year":"2002"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib41","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1145\/377978.377993","article-title":"Weak alternating automata are not that weak","volume":"2","author":"Kupferman","year":"2001","journal-title":"ACM Trans, on Computational Logic"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib42","doi-asserted-by":"crossref","first-page":"312","DOI":"10.1145\/333979.333987","article-title":"An automata-theoretic approach to branching-time model checking","volume":"47","author":"Kupferman","year":"2000","journal-title":"Journal of the ACM"},{"key":"10.1016\/S1570-2464(07)80020-6_bib43","series-title":"Proc. 7th ACM Symp. on Principles of Programming Languages","first-page":"174","article-title":"Sometimes is sometimes \u201cnot never\u201d \u2014 on the temporal logic of programs","author":"Lamport","year":"1980"},{"key":"10.1016\/S1570-2464(07)80020-6_bib44","series-title":"Proc. 12th ACM Symp. on Principles of Programming Languages","first-page":"97","article-title":"Checking that finite state concurrent programs satisfy their linear specification","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib45","series-title":"Logics of Programs","first-page":"196","article-title":"The glory of the past","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib46","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/S0065-2458(08)60533-1","article-title":"Protocol engineering","volume":"29","author":"Liu","year":"1989","journal-title":"Advances in Computing"},{"key":"10.1016\/S1570-2464(07)80020-6_bib47","series-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna","year":"1992"},{"key":"10.1016\/S1570-2464(07)80020-6_bib48","article-title":"Temporal specification and verification of reactive modules","author":"Manna","year":"1992"},{"key":"10.1016\/S1570-2464(07)80020-6_bib49","series-title":"Proc. 11th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems","first-page":"222","article-title":"Using BDDs to decide ctl","author":"Marrero","year":"2005"},{"key":"10.1016\/S1570-2464(07)80020-6_bib50","series-title":"Complementation is more difficult with automata on infinite words","author":"Michel","year":"1988"},{"key":"10.1016\/S1570-2464(07)80020-6_bib51","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","article-title":"Alternating finite automata on \u03c9-words","volume":"32","author":"Miyano","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib52","series-title":"Computation Theory","first-page":"157","article-title":"Regular expressions for infinite trees and a standard form of automata","author":"Mostowski","year":"1984"},{"key":"10.1016\/S1570-2464(07)80020-6_bib53","series-title":"Proceedings 3rd IEEE Symp. on Logic in Computer Science","first-page":"422","article-title":"Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time","author":"Muller","year":"1988"},{"key":"10.1016\/S1570-2464(07)80020-6_bib54","series-title":"Proc. 13th International Colloquium on Automata, Languages and Programming","first-page":"275","article-title":"Alternating automata, the weak monadic theory of the tree and its complexity","author":"M\u00fcller","year":"1986"},{"key":"10.1016\/S1570-2464(07)80020-6_bib55","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","article-title":"Alternating automata on infinite trees","volume":"54","author":"Muller","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib56","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/0304-3975(94)00214-4","article-title":"Simulating alternating tree automata by nondeterministic automata: New results and new proofs of theorems of Rabin, McNaughton and Safra","volume":"141","author":"Muller","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib57","series-title":"Proc. 18th IEEE Symp. on Foundation of Computer Science","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/S1570-2464(07)80020-6_bib58","series-title":"Proc. 12th International Colloquium on Automata, Languages and Programming","first-page":"15","article-title":"Linear and branching structures in the semantics and logics of reactive systems","author":"Pnueli","year":"1985"},{"key":"10.1016\/S1570-2464(07)80020-6_bib59","series-title":"Time and Modality","author":"Prior","year":"1957"},{"key":"10.1016\/S1570-2464(07)80020-6_bib60","series-title":"Proc. 5th International Symp. on Programming","first-page":"337","article-title":"Specification and verification of concurrent systems in Cesar","author":"Queille","year":"1981"},{"key":"10.1016\/S1570-2464(07)80020-6_bib61","first-page":"1","article-title":"Decidability of second order theories and automata on infinite trees","volume":"141","author":"Rabin","year":"1969","journal-title":"Transaction of the AMS"},{"key":"10.1016\/S1570-2464(07)80020-6_bib62","series-title":"Proc. Symp. Math. Logic and Foundations of Set Theory","first-page":"1","article-title":"Weakly definable relations and special automata","author":"Rabin","year":"1970"},{"key":"10.1016\/S1570-2464(07)80020-6_bib63","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1146\/annurev.cs.02.060187.001451","article-title":"Network protocols and tools to help produce them","volume":"2","author":"Rudin","year":"1987","journal-title":"Annual Review of Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib64","series-title":"Proc. 1st Int'l Joint Conf. on Automated Reasoning","first-page":"76","article-title":"The hybrid \u03bc-calculus","author":"Sattler","year":"2001"},{"key":"10.1016\/S1570-2464(07)80020-6_bib65","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","article-title":"Relationship between nondeterministic and deterministic tape complexities","volume":"4","author":"Savitch","year":"1970","journal-title":"Journal on Computer and System Sciences"},{"key":"10.1016\/S1570-2464(07)80020-6_bib66","article-title":"Theoretical issues in the design of distributed and concurrent systems","author":"Sistla","year":"1983"},{"key":"10.1016\/S1570-2464(07)80020-6_bib67","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logic","volume":"32","author":"Sistla","year":"1985","journal-title":"Journal ACM"},{"key":"10.1016\/S1570-2464(07)80020-6_bib68","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0304-3975(87)90008-9","article-title":"The complementation problem for B\u00fcchi automata with applications to temporal logic","volume":"49","author":"Sistla","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1570-2464(07)80020-6_bib69","first-page":"465","article-title":"An elementary decision procedure for the \u03bc-calculus","volume":"volume 172","author":"Street","year":"1984"},{"key":"10.1016\/S1570-2464(07)80020-6_bib70","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","article-title":"Propositional dynamic logic of looping and converse","volume":"54","author":"Streett","year":"1982","journal-title":"Information and Control"},{"issue":"2","key":"10.1016\/S1570-2464(07)80020-6_bib71","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","article-title":"Depth first search and linear graph algorithms","volume":"1","author":"Tarjan","year":"1972","journal-title":"SIAM Journal of Computing"},{"key":"10.1016\/S1570-2464(07)80020-6_bib72","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/BF01691346","article-title":"Generalized finite automata theory with an application to a decision problem of second-order logic","volume":"2","author":"Thatcher","year":"1968","journal-title":"Mathematical System Theory"},{"key":"10.1016\/S1570-2464(07)80020-6_bib73_1","first-page":"101","article-title":"Finite automata and monadic second order logic","volume":"3","author":"Trakhtenbrot","year":"1962","journal-title":"Siberian Math. J"},{"key":"10.1016\/S1570-2464(07)80020-6_bib73_2","first-page":"23","article-title":"Finite automata and monadic second order logic","volume":"59","author":"Trakhtenbrot","year":"1966","journal-title":"AMS Transi"},{"key":"10.1016\/S1570-2464(07)80020-6_bib74","series-title":"Proc. International Symp. on The- oretical Aspects of Computer Software","first-page":"575","article-title":"Nontraditional applications of automata theory","author":"Vardi","year":"1994"},{"key":"10.1016\/S1570-2464(07)80020-6_bib75","series-title":"Computer Science Today -Recent Trends and Developments","first-page":"471","article-title":"Alternating automata and program verification","author":"Vardi","year":"1994"},{"key":"10.1016\/S1570-2464(07)80020-6_bib76","series-title":"Proc. 13th IEEE Sym. on Logic in Computer Science","first-page":"394","article-title":"Linear vs. branching time: A complexity-theoretic perspective","author":"Vardi","year":"1998"},{"key":"10.1016\/S1570-2464(07)80020-6_bib77","series-title":"Proc. 25th International Coll. on Automata, Languages, and Programming","first-page":"628","article-title":"Reasoning about the past with two-way automata","author":"Vardi","year":"1998"},{"key":"10.1016\/S1570-2464(07)80020-6_bib78","series-title":"Proc. 9th Int'l Conf. on Concurrency Theory","first-page":"1","article-title":"Sometimes and not never re-revisited: on branching vs. linear time","author":"Vardi","year":"1998"},{"key":"10.1016\/S1570-2464(07)80020-6_bib79","series-title":"Proc. 7th International Conference on Tools and algorithms for the construction and analysis of systems","first-page":"1","article-title":"Branching vs. linear time: Final showdown","author":"Vardi","year":"2001"},{"key":"10.1016\/S1570-2464(07)80020-6_bib80","series-title":"Logics of Programs","first-page":"501","article-title":"Yet another process logic","author":"Vardi","year":"1984"},{"key":"10.1016\/S1570-2464(07)80020-6_bib81","series-title":"Proc. 1st Symp. on Logic in Computer Science","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986"},{"key":"10.1016\/S1570-2464(07)80020-6_bib82","first-page":"182","article-title":"Automata-theoretic techniques for modal logics of programs","volume":"32","author":"Vardi","year":"1986"},{"issue":"1","key":"10.1016\/S1570-2464(07)80020-6_bib83","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","article-title":"Reasoning about infinite computations","volume":"115","author":"Vardi","year":"1994","journal-title":"Information and Computation"},{"issue":"4","key":"10.1016\/S1570-2464(07)80020-6_bib84","first-page":"350","article-title":"Practical CTL* model checking: Should SPIN be extended?","volume":"2","author":"Visser","year":"2000","journal-title":"Interna- tional Journal on Software Tools for Technology Transfer"},{"key":"10.1016\/S1570-2464(07)80020-6_bib85","series-title":"Proc. 24th IEEE Symp. on Foundations of Computer Science","first-page":"185","article-title":"Reasoning about infinite computation paths","author":"Wolper","year":"1983"}],"container-title":["Studies in Logic and Practical Reasoning","Handbook of Modal Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800206?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1570246407800206?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T23:14:54Z","timestamp":1761606894000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1570246407800206"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9780444516909"],"references-count":86,"URL":"https:\/\/doi.org\/10.1016\/s1570-2464(07)80020-6","relation":{},"ISSN":["1570-2464"],"issn-type":[{"value":"1570-2464","type":"print"}],"subject":[],"published":{"date-parts":[[2007]]}}}