{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T16:53:13Z","timestamp":1694623993485},"reference-count":20,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[1992,5,1]],"date-time":"1992-05-01T00:00:00Z","timestamp":704678400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[1992,5]]},"abstract":"Abstract<\/jats:title>\n This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.<\/jats:p>","DOI":"10.1007\/bf01212306","type":"journal-article","created":{"date-parts":[[2005,2,25]],"date-time":"2005-02-25T13:00:49Z","timestamp":1109336449000},"page":"299-319","source":"Crossref","is-referenced-by-count":2,"title":["A model checker for linear time temporal logic"],"prefix":"10.1145","volume":"4","author":[{"given":"Michael","family":"Fisher","sequence":"first","affiliation":[{"name":"The TEMPLE Group, Department of Computer Science, University of Manchester, UK"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Banieqbal B.: The Problem of Verifying Systems with Many Processes. TEMPLE project report Department of Computer Science University of Manchester 1987."},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Barringer H. Fisher M. and Gough G.: Fair SMG and Linear Time Model Checking. In Proc. Workshop on Automatic Verification Methods for Finite State Systems Grenoble France June 1989. (Published in Lecture Notes in Computer Science 407.)","DOI":"10.1007\/3-540-52148-8_12"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Barringer H. Kuiper R. and Pnueli A.: A Really Abstract Concurrent Model and its Temporal Logic. In Proc. 13th ACM Symp. on the Principles of Programming Languages St. Petersberg Beach Florida January 1986.","DOI":"10.1145\/512644.512660"},{"key":"e_1_2_1_2_4_2","unstructured":"Browne M.C.: An Improved Algorithm for the Automatic Verification of Finite State Systems using Temporal Logic. Technical report Department of Computer Science Carnegie Mellon University December 1986."},{"key":"e_1_2_1_2_5_2","unstructured":"Browne M.C Clarke E.M. Dill D. and Mishra B.: Automatic Verification of Sequential Circuits using Temporal Logic. Technical Report CS-85-100 Department of Computer Science Carnegie Mellon University 1984."},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Clarke E.M. and Gr\u00fcmberg O.: Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms. Technical report Department of Computer Science Carnegie Mellon University 1987.","DOI":"10.1145\/41840.41865"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Clarke E.M. Emerson E.A. and Sistla A.P.: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach. In Proc. 10th ACM Symp. on the Principles of Programming Languages Austin Texas 1983.","DOI":"10.1145\/567067.567080"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Clarke E. M. Gr\u00fcmberg O. and Browne M. C.: Reasoning about Networks with many identical Finite-State Processes. Technical report Department of Computer Science Carnegie Mellon University December 1986.","DOI":"10.21236\/ADA188743"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Emerson E. A. and Halpern J. Y.: Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. In Proc. 14th ACM Symp. on the Theory of Computing pp. 169\u2013180 1982.","DOI":"10.1145\/800070.802190"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(84)80047-9"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_2_1_2_12_2","volume-title":"Characterising Temporal Logic. Technical Report UMCS-89-10-6","author":"Fisher M.","year":"1989"},{"key":"e_1_2_1_2_13_2","unstructured":"Gough G. D.: Decision Procedures for Temporal Logic. Master's thesis Department of Computer Science University of Manchester October 1984."},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Gough G. D. and Barringer H.: A Semantics Driven Temporal Verification System. In Proc. ESOP '88 March 1988.","DOI":"10.1007\/3-540-19027-9_2"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Lichtenstein O. and Pnueli A.: Checking that Finite State Concurrent Programs Satisfy their Linear Specification. In Proc. 12th ACM Symposium on the Principles of Programming Languages New Orleans Louisiana January 1985.","DOI":"10.1145\/318593.318622"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Lichtenstein O. Pnueli A. and Zuck L.: The Glory of the Past. Lecture Notes in Computer Science 193 pp. 196\u2013218 Springer-Verlag 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Pnueli A.: The Temporal Logic of Programs. In Proc. 18th Symp. on the Foundations of Computer Science Providence November 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/3828.3837"},{"key":"e_1_2_1_2_19_2","unstructured":"Stroustrup B.: The C++ Programming Language Addison-Wesley 1986."},{"key":"e_1_2_1_2_20_2","volume-title":"Technical Report RJ 5184 (53488)","author":"Vardi M. Y.","year":"1986"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01212306.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01212306\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/BF01212306","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:22:42Z","timestamp":1641482562000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/BF01212306"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,5]]},"references-count":20,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1992,5]]}},"alternative-id":["10.1007\/BF01212306"],"URL":"https:\/\/doi.org\/10.1007\/bf01212306","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,5]]}}}