{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,12]],"date-time":"2023-01-12T00:48:09Z","timestamp":1673484489481},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,7,8]],"date-time":"2006-07-08T00:00:00Z","timestamp":1152316800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s10703-006-0009-y","type":"journal-article","created":{"date-parts":[[2006,7,7]],"date-time":"2006-07-07T13:27:54Z","timestamp":1152278874000},"page":"117-134","source":"Crossref","is-referenced-by-count":8,"title":["Distributed breadth-first search LTL model checking"],"prefix":"10.1007","volume":"29","author":[{"given":"Ji\u0159\u00ed","family":"Barnat","sequence":"first","affiliation":[]},{"given":"Ivana","family":"\u010cern\u00e1","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,7,8]]},"reference":[{"key":"9_CR1","unstructured":"Barnat J, Brim L, \u010cerna\u00b4 I (2002) Property driven distribution of nested DFS. In: Proceeding of the 3rd International Workshop on Verification and Computational Logic (VCL'2002). DSSE Technical Report, Pittsburgh, PA, USA, pp 1\u201310"},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Barnat J, Brim L, St\u0159\u00edbrn\u00b4 J (2001) Distributed LTL model-checking in SPIN. In: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, vol 2057 of LNCS, Springer, pp 200\u2013216","DOI":"10.1007\/3-540-45139-0_13"},{"key":"9_CR3","unstructured":"Barnat J, Brim L, \u010cern\u00b4 I, \u0160ime\u010dek P (July 2005) DiVinE\u2014The distributed verification environment. In: Proceedings of 4th International Workshop on Parallel and Distributed Methods in verifiCation, pp 89\u201394"},{"key":"9_CR4","unstructured":"Barnat J (2004) Distributed memory LTL model checking. PhD thesis, Faculty of Informatics, Masaryk University Brno"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Brim L, \u010cern\u00e1 I, Kr\u010d\u00e1l P, Pel\u00e1nek R (2001) Distributed LTL model checking based on negative cycle detection. In: Proceedings of Foundations of Software Technology and Theoretical Computer Science (FST\u2013TCS'01), volume 2245 of LNCS, Springer, pp 96\u2013107","DOI":"10.1007\/3-540-45294-X_9"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Brim L, \u010cern\u00e1 I, Moravec P, \u0160im\u0161a J (2004) Accepting predecessors are better than back edges in distributed ltl model-checking. In: Formal Methods in Computer-Aided Design (FMCAD), volume 3312 of LNCS, Springer, pp 352\u2013366","DOI":"10.1007\/978-3-540-30494-4_25"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Brim L, \u010cern\u00e1 I, Moravec P, \u0160im\u0161a J (April 2005) Distributed partial order reduction. Electr Notes Theoret Comput Sci., 128:63\u201374","DOI":"10.1016\/j.entcs.2004.10.019"},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1 I, \u00a0Pel\u00e1nek R (2003) Distributed explicit fair cycle detection (set based approach). In: Model Checking Software. 10th International SPIN Workshop, volume 2648 of LNCS, Springer, pp 49\u201373","DOI":"10.1007\/3-540-44829-2_4"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"\u010cern\u00e1 I, Pel\u00e1nek R (2003) Relating hierarchy of temporal properties to model checking. In: Mathematical Foundations of Computer Science (MFCS), volume 2747 of LNCS, Springer, pp 318\u2013327","DOI":"10.1007\/978-3-540-45138-9_26"},{"key":"9_CR10","unstructured":"Clarke EM, Grumberg O, Peled DA (1999) Model Checking, The MIT Press, Cambridge, Massachusetts"},{"key":"9_CR11","doi-asserted-by":"crossref","unstructured":"Courcoubetis C, Vardi M, Wolper P, Yannakakis M (1992) Memory-efficient algorithms for the verification of temporal properties. Formal Methods System Designxy, 1:275\u2013288","DOI":"10.1007\/BF00121128"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Dwyer MB, Avrunin GS, Corbett JC (1998) Property specification patterns for finite-state verification. In: Proc. Workshop on Formal Methods in Software Practice, ACM Press, pp 7\u201315","DOI":"10.1145\/298595.298598"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Edelkamp S, Lluch-Lafuente A, Leue S (2001) Directed model-checking in HSF-SPIN. In: Matthew B. Dwyer (ed), 8th International SPIN Workshop, number 2057 in LNCS, Springer, pp 57\u201379","DOI":"10.1007\/3-540-45139-0_5"},{"key":"9_CR14","unstructured":"Hojati R, Touati H, Kurshan RP, Brayton RK (1992) Efficient omega-regular language containment. In: Computer Aided Verification, volume 663 of LNCS, Springer, pp 396\u2013409."},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Holzmann GJ (1997) The model checker SPIN. IEEE Trans Softw Eng 23(5):279\u2013295","DOI":"10.1109\/32.588521"},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"Lerda F, Sisto R (1999) Distributed-memory model checking with SPIN. In: Proc. of the 5th International SPIN Workshop, volume 1680 of LNCS, Springer","DOI":"10.1007\/3-540-48234-2_3"},{"key":"9_CR17","unstructured":"Pnueli A (1981) The temporal logic of conurrent programs. Theoret. Comput Sci 13:45\u201360"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Vardi MY, Wolper P (1986) Automata theoretic techniques for modal logics of programs. J Comput System Sci 32:183\u2013221","DOI":"10.1016\/0022-0000(86)90026-7"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0009-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0009-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0009-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:02Z","timestamp":1559253662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0009-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,8]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["9"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0009-y","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,7,8]]}}}