{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T08:17:32Z","timestamp":1648801052344},"reference-count":18,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(05)80095-7","type":"journal-article","created":{"date-parts":[[2005,5,25]],"date-time":"2005-05-25T12:37:08Z","timestamp":1117024628000},"page":"33-50","source":"Crossref","is-referenced-by-count":3,"title":["Distributed Explicit Bounded LTL Model Checking"],"prefix":"10.1016","volume":"89","author":[{"given":"Pavel","family":"Kr\u010d\u00e1l","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(05)80095-7_BIB1","series-title":"Proc. SPIN Workshop on Model Checking of Software, volume 2057 of LNCS","first-page":"200","article-title":"Distributed LTL Model-Checking in SPIN","author":"Barnat","year":"2001"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB2","series-title":"Proc. Workshop on Verification and Computational Logic, number DSSE- TR-2002-5 in DSSE Technical Report","first-page":"1","article-title":"Property driven distribution of Nested DFS","author":"Barnat","year":"2002"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB3","series-title":"Tools Algorithms for the Construction and Analysis of Systems. Part of European Conferences on Theory and Practice of Software, ETAPS'99, Amsterdam, volume 1579 of LNCS","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"Biere","year":"1999"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB4","series-title":"Proceedings of the 9th International SPIN Workshop on Model checking of Software (SPIN '02), volume 2318 of LNCS","article-title":"Local parallel model checking for the alternation-free mu-calculus","author":"Bollig","year":"2002"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB5","series-title":"Proc. Foundations of Software Technology and Theoretical Computer Science, volume 2245 of LNCS","first-page":"96","article-title":"Distributed LTL model checking based on negative cycle detection","author":"Brim","year":"2001"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB6","article-title":"Using assumptions to distribute CTL model checking","volume":"volume 68","author":"Brim","year":"2002"},{"issue":"2","key":"10.1016\/S1571-0661(05)80095-7_BIB7","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\/S1571-0661(05)80095-7_BIB8","series-title":"Proc. SPIN workshop, number 2648 in LNCS","article-title":"Distributed explicit fair cycle detection","author":"\u010cern\u00e1","year":"2003"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB9","series-title":"Model Checking","author":"Clarke","year":"1999"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB10","first-page":"200","article-title":"Parallel state space construction for model-checking","volume":"2057","author":"Garavel","year":"2001","journal-title":"Lecture Notes in Computer Science"},{"issue":"5","key":"10.1016\/S1571-0661(05)80095-7_BIB11","first-page":"279","article-title":"The model checker SPIN., IEEE Transactions on Software","volume":"23","author":"Holzmann","year":"1997","journal-title":"Engineering"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB12","series-title":"ICALP: Annual International Colloquium on Automata, Languages and Programming","article-title":"Algorithmic verification of linear temporal logic specifications","author":"Kesten","year":"1998"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB13","article-title":"Distributed explicit bounded LTL model checking","author":"Kr\u010d\u00e1l","year":"2003","journal-title":"Master's thesis, Masaryk University Brno"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB14","series-title":"Proc. Tools and Algorithms for Construction and Analysis of Systems, volume 2280 of LNCS","first-page":"1","article-title":"Software construction and analysis tools for future space missions","author":"Lowry","year":"2002"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB15","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF01782776","article-title":"Algorithms for distributed termination detection","volume":"2, 3","author":"Mattern","year":"1987","journal-title":"Distributed Computing"},{"issue":"5","key":"10.1016\/S1571-0661(05)80095-7_BIB16","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/0020-0190(85)90024-9","article-title":"Depth-first search is inherrently sequential","volume":"20","author":"Reif","year":"1985","journal-title":"Information Processing Letters"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB17","series-title":"Introduction to Distibuted Algorithms","author":"Tel","year":"1994"},{"key":"10.1016\/S1571-0661(05)80095-7_BIB18","series-title":"Proc. LICS 1986","first-page":"332","article-title":"An automata-theoretic approach to automatic program verification","author":"Vardi","year":"1986"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800957?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066105800957?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,26]],"date-time":"2019-01-26T08:58:30Z","timestamp":1548493110000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066105800957"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066105800957"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(05)80095-7","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}