{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T05:21:45Z","timestamp":1738387305575,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540705437"},{"type":"electronic","value":"9783540705451"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-70545-1_48","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"504-516","source":"Crossref","is-referenced-by-count":12,"title":["Discriminative Model Checking"],"prefix":"10.1007","author":[{"given":"Peter","family":"Niebert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"48_CR1","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1007\/BF01782772","volume":"2","author":"B. Alpern","year":"1987","unstructured":"Alpern, B., Schneider, F.B.: Recognizing Safety and Liveness. Distributed Computing\u00a02, 117\u2013126 (1987)","journal-title":"Distributed Computing"},{"key":"48_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"48_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing Correctness Properties of Parallel Programs using Fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"key":"48_CR4","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.L.: Modalities for Model Checking. Science of Computer Programming\u00a08, 275\u2013306 (1987)","journal-title":"Science of Computer Programming"},{"key":"48_CR5","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10009-005-0202-0","volume":"8","author":"A. Groce","year":"2006","unstructured":"Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error Explanation with Distance Metrics. STTT\u00a08, 229\u2013247 (2006)","journal-title":"STTT"},{"key":"48_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/3-540-46002-0_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Jin","year":"2002","unstructured":"Jin, H., Ravi, K., Somenzi, F.: Fate and Free Will in Error Traces. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol.\u00a02280, pp. 445\u2013459. Springer, Heidelberg (2002)"},{"key":"48_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1007\/978-3-540-78800-3_11","volume-title":"TACAS 2008","author":"G. Katz","year":"2008","unstructured":"Katz, G., Peled, D.: Model Checking Based Genetic Programming with an Application to Mutual Exclusion. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 141\u2013156. Springer, Heidelberg (2008)"},{"key":"48_CR8","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Memoryful Branching Time Logic. In: LICS 2006, Seatle, USA, pp. 265\u2013274 (2006)","DOI":"10.1109\/LICS.2006.34"},{"key":"48_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/3-540-48683-6_17","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Model Checking Safety Properties. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 172\u2013183. Springer, Heidelberg (1999)"},{"key":"48_CR10","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"48_CR11","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The Temporal Logic of Programs. In: 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"48_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the Synthesis of Reactive Systems. In: POPL 1989, Austin, Texas, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"48_CR13","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and Verification of Concurrent Systems in CESAR. In: 5th International Symposium on Programming, pp. 337\u2013350 (1981)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"48_CR14","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"W.J. Savitch","year":"1970","unstructured":"Savitch, W.J.: Relationships between Nondeterministic and Deterministic Tape Complexities. Journal of Computer and System Science\u00a04, 177\u2013192 (1970)","journal-title":"Journal of Computer and System Science"},{"key":"48_CR15","unstructured":"Shahar, E.: The TLV System and its Applications, M.Sc. Thesis, The Weizmann Institute of Science"},{"key":"48_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/3-540-45251-6_35","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"N. Sharygina","year":"2001","unstructured":"Sharygina, N., Peled, D.: A Combined testing and Verification Approach for Software Reliability. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol.\u00a02021, pp. 611\u2013628. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70545-1_48","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:12:43Z","timestamp":1738325563000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70545-1_48"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540705437","9783540705451"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70545-1_48","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}