{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T05:27:48Z","timestamp":1747805268190,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540410300"},{"type":"electronic","value":"9783540452973"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722468_12","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T11:43:32Z","timestamp":1167479012000},"page":"187-204","source":"Crossref","is-referenced-by-count":7,"title":["Abstraction of Communication Channels in Promela: A Case Study"],"prefix":"10.1007","author":[{"given":"Elena","family":"Fersman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., \u010cer\u01cens, K., Jonsson, B., Yih-Kuen, T.: General decidability theorems for infinite-state systems. In: Proc. 11th IEEE Int. Symp. on Logic in Computer Science, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unre- liable channels. Information and Computation\u00a0127(2), 91\u2013101 (1996)","journal-title":"Information and Computation"},{"issue":"2","key":"12_CR3","first-page":"190","volume":"COM-24","author":"D. Belsnes","year":"1976","unstructured":"Belsnes, D.: Single-message communication. IEEE Trans. on Computers\u00a0COM-24(2), 190\u2013194 (1976)","journal-title":"IEEE Trans. on Computers"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing abstractions of infinite state systems automatically and compositionally. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symp. on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. on Programming Languages and Systems\u00a016(5) (September 1994)","DOI":"10.1145\/186025.186051"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer Aided Verification","author":"M.A. Colon","year":"1998","unstructured":"Colon, M.A., Uribe, T.E.: Generating finite-state abstractions of re- active systems using decision procedures. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-48683-6_16","volume-title":"Computer Aided Verification","author":"S. Das","year":"1999","unstructured":"Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 160\u2013171. Springer, Heidelberg (1999)"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Transactions on Programming Languages and Systems\u00a019(2) (1997)","DOI":"10.1145\/244795.244800"},{"key":"12_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"issue":"2","key":"12_CR11","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1006\/inco.1993.1069","volume":"107","author":"B. Jonsson","year":"1993","unstructured":"Jonsson, B., Parrow, J.: Deciding bisimulation equivalences for a class of non-finite-state programs. Information and Computation\u00a0107(2), 272\u2013302 (1993)","journal-title":"Information and Computation"},{"issue":"2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/BF01786631","volume":"4","author":"L. Lamport","year":"1990","unstructured":"Lamport, L.: A theorem on atomicity in distributed algorithms. Distri- buted Computing\u00a04(2), 59\u201368 (1990)","journal-title":"Distri- buted Computing"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Lesens, D., Saidi, H.: Abstraction of parameterized networks. Electronic Notes in Theoretical Computer Science, 9 (1997)","DOI":"10.1016\/S1571-0661(05)80429-3"},{"key":"12_CR14","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann Publishers, San Francisco (1996)"},{"key":"12_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems. Springer, Heidelberg (1992)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/3-540-48683-6_38","volume-title":"Computer Aided Verification","author":"H. Saidi","year":"1999","unstructured":"Saidi, H., Shankar, N.: Abstract and model check while you prove. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 443\u2013454. Springer, Heidelberg (1999)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Pierre Wolper. Expressing interesting properties of programs in proposi- tional temporal logic (extended abstract). In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 184{193, Jan. 1986.","DOI":"10.1145\/512644.512661"}],"container-title":["Lecture Notes in Computer Science","SPIN Model Checking and Software Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722468_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T19:08:01Z","timestamp":1736708881000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722468_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540410300","9783540452973"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10722468_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}