{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:22:57Z","timestamp":1759638177481},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"6-7","license":[{"start":{"date-parts":[[1992,6,1]],"date-time":"1992-06-01T00:00:00Z","timestamp":707356800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1992,6]]},"DOI":"10.1007\/bf01185559","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T16:12:06Z","timestamp":1108743126000},"page":"523-543","source":"Crossref","is-referenced-by-count":22,"title":["An experience in proving regular networks of processes by modular model checking"],"prefix":"10.1007","volume":"29","author":[{"given":"Nicolas","family":"Halbwachs","sequence":"first","affiliation":[]},{"given":"Fabienne","family":"Lagnier","sequence":"additional","affiliation":[]},{"given":"Christophe","family":"Ratel","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"[AK86] Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent system. Inf. Process. Lett.22, 307?309 (1986)","journal-title":"Inf. Process. Lett."},{"key":"CR2","unstructured":"[BCM+89] Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, J.: Symbolic model checking: 1020 states and beyond. Technical report, Carnegie Mellon University, 1989"},{"key":"CR3","series-title":"Technical Report SPECTRE","volume-title":"On the verification of safety properties","author":"A. Bouajjani","year":"1990","unstructured":"[BFH90] Bouajjani, A., Fernandez, J.C., Halbwachs, N.: On the verification of safety properties. Technical Report SPECTRE L12, IMAG, Grenoble, March 1990"},{"issue":"8","key":"CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"[Bry86] Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput.C-35(8), 677?691 (1986)","journal-title":"IEEE Trans. Comput. C"},{"key":"CR5","series-title":"Lect. Notes Comput. Sci.","volume-title":"International Workshop on Automatic Verification Methods for Finite Sate Systems","author":"O. Coudert","year":"1989","unstructured":"[CBM89] Coudert, O., Berthet, C., Madre, J.C.: Verification of synchronous sequential machines based on symbolic execution. International Workshop on Automatic Verification Methods for Finite Sate Systems. (Lect. Notes Comput. Sci., vol. 407) Berlin Heidelberg New York: Springer 1989"},{"issue":"2","key":"CR6","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"[CES86] Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. TOPLAS8(2), 244?263 (1986)","journal-title":"TOPLAS"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"[CGB86] Clarke, E.M., Grumberg, O., Browne, M.C.: Reasonning about networks with many identical finite-state processes. ACM Symposium on Principles of Distributed Computing, Calgary (Alberta), p. 240?248, August 1986","DOI":"10.1145\/10590.10611"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"[CLM89] Clarke, E.M., Long, D.E., Mc Millan, K.L.: Compositional model checking. In: Fourth IEEE Symposium on Logic in Computer Science, June 1989","DOI":"10.1109\/LICS.1989.39190"},{"key":"CR9","unstructured":"[CMB90] Coudert, O., Madre, J.C., Berthet, C.: Verifying temporal properties of sequential machines without building their state diagrams. International Workshop on Computer-Aided Verification, June 1990"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"[CPHP87] Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. 14th ACM Symposium on Principles of Programming Languages, January 1987","DOI":"10.1145\/41625.41641"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"[FM91] Fernandez, J.C., Mounier, L.: On the fly verification of behavioural equivalences and preorders. Workshop on Computer-Aided Verification, Aalborg (Denmark), June 1991","DOI":"10.1007\/3-540-55179-4_18"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"[GS90] Graf, S., Steffen, B.: Compositional minimization of finite state systems. Workshop on Computer-Aided Verification, June 1990","DOI":"10.1090\/dimacs\/003\/06"},{"issue":"9","key":"CR13","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"[HCRP91] Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous dataflow programming language LUSTRE. Proceedings of the IEEE79(9): 1305?1320, September 1991","journal-title":"Proceedings of the IEEE"},{"issue":"6","key":"CR14","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1109\/TSE.1987.233206","volume":"13","author":"G.J. Holzmann","year":"1987","unstructured":"[Hol87] Holzmann, G.J.: Automated protocol validation in ARGOS: Assertion proving and scatter searching. IEEE Trans. Software EngSE-13(6), 683?696 (1987)","journal-title":"IEEE Trans. Software Eng SE"},{"key":"CR15","series-title":"Lect. Notes Comput. Sci.","first-page":"213","volume-title":"Workshop on Automatic Verification Methods for Finite State Systems","author":"N. Halbwachs","year":"1989","unstructured":"[HPOG89] Halbwachs, N., Pilaud, D., Ouabdesselam, F., Glory, A.C.: Specifying, programming and verifying real-time systems, using a synchronous declarative language. Workshop on Automatic Verification Methods for Finite State Systems. (Lect. Notes Comput. Sci., vol. 407, pp. 213?231). Berlin Heidelberg New York: Springer 1989"},{"key":"CR16","series-title":"Lect. Notes Comput. Sci.","volume-title":"International Workshop on Automatic Verification Methods for Finite State Systems","author":"C. Jard","year":"1989","unstructured":"[JJ89] Jard, C., J\u00e9ron, Th.: On-line model checking for finite linear temporal logic specifications. International Workshop on Automatic Verification Methods for Finite State Systems. (Lect. Notes Comput. Sci., vol. 407). Berlin Heidelberg New York: Springer 1989"},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"[KM89] Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. 8th AC Symposium on Principles of Distributed Computing, Edmonton (Alberta), p. 239?247, August 1989","DOI":"10.1145\/72981.72998"},{"key":"CR18","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Conference on Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"[LPZ85] Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. Conference on Logics of Programs. (Lect. Notes Comput. Sci., vol. 194, pp. 196?218). Berlin Heidelberg New York: Springer 1985"},{"key":"CR19","series-title":"Lect. Notes Comput. Sci.","first-page":"201","volume-title":"Linear time, branching time and partial orders in logics and models for concurrency","author":"Z. Manna","year":"1988","unstructured":"[MP88] Manna, Z., Pnueli, A.: The anchored version of the temporal framework. In: Roever W.P. de, Bakker, J.W. de, Rozenberg, G. (eds.) Linear time, branching time and partial orders in logics and models for concurrency. (Lect. Notes Comput. Sci., vol. 354, pp. 201?284). Berlin Heidelberg New York: Springer 1988"},{"key":"CR20","series-title":"Lect. Notes Comput. Sci.","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"[QS82] Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. International Symposium on Programming. (Lect. Notes Comput. Sci., vol. 137, pp. 337?351. Berlin Heidelberg New York: Springer 1982"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"[RHR91] Ratel, C., Halbwachs, N., Raymond, P.: Programming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE. ACMSIGSOFT'91 Conference on Software for Critical Systems. New Orleans, December 1991","DOI":"10.1145\/125083.123062"},{"key":"CR22","volume-title":"IFIP WG-6.1 7th. International Conference on Protocol Specification, Testing and Verification","author":"J.L. Richier","year":"1987","unstructured":"[RRSV87] Richier, J.L., Rodriguez, C., Sifakis, J., Voiron, J.: Verification in XESAR of the sliding window protocol. IFIP WG-6.1 7th. International Conference on Protocol Specification, Testing and Verification. Amsterdam: North Holland 1987"},{"key":"CR23","unstructured":"[SG87] Sistla, A.P., German, S.M.: Reasoning with many processes. Symposium on Logic in Computer Science, Ithaca, p. 138?152, June 1987"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I. Suzuki","year":"1988","unstructured":"[Suz88] Suzuki, I.: Proving properties of a ring of finite-state machines. Int. Process. Lett.28, 213?214 (1988)","journal-title":"Int. Process. Lett."},{"key":"CR25","series-title":"Lect. Notes Comput. Sci.","first-page":"68","volume-title":"International Workshop on Automatic Verification Methods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"[WL89] Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. International Workshop on Automatic Verification Methods for Finite State Systems. (Lect. Notes Comput. Sci., vol. 407, pp. 68?80). Berlin Heidelberg New York: Springer 1989"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01185559.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01185559\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01185559","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T21:15:44Z","timestamp":1586121344000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01185559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992,6]]},"references-count":25,"journal-issue":{"issue":"6-7","published-print":{"date-parts":[[1992,6]]}},"alternative-id":["BF01185559"],"URL":"https:\/\/doi.org\/10.1007\/bf01185559","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992,6]]}}}