{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T09:37:26Z","timestamp":1773653846689,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540638889","type":"print"},{"value":"9783540696612","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0000481","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T06:30:36Z","timestamp":1128493836000},"page":"337-350","source":"Crossref","is-referenced-by-count":2,"title":["Invariants of parameterized binary tree networks as greatest fixpoints"],"prefix":"10.1007","author":[{"given":"David","family":"Lesens","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,9,7]]},"reference":[{"key":"23_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":"K. R. Apt and D. C. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 22:307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"issue":"2","key":"23_CR2","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87\u2013152, 1992.","journal-title":"Science of Computer Programming"},{"key":"23_CR3","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In 4 th ACM Symposium on Principles of Programming Languages, POPL '77, Los Angeles, January 1977.","DOI":"10.1145\/512950.512973"},{"key":"23_CR4","series-title":"LNCS 631","volume-title":"PLILP'92","author":"P. Cousot","year":"1992","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and widening\/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, PLILP'92, Leuven (Belgium), January 1992. LNCS 631, Springer Verlag."},{"key":"23_CR5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM TOPLAS, 8(2), 1986.","DOI":"10.1145\/5397.5399"},{"key":"23_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and S. Jha. Verifying parameterized networks using abstraction and regular languages. In CONCUR'95. LNCS 962, Springer Verlag, August 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"23_CR7","unstructured":"S. Eilenberg. Automata, Languages, and Machines. Academic Press, 1974."},{"key":"23_CR8","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In Proc. 22th ACM Conf. on Principles of Programming Languages, POPL'95, San Francisco, January 1995.","DOI":"10.1145\/199448.199468"},{"key":"23_CR9","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Automatic verification of parameterized synchronous systems. In R. Alur and T. Henzinger, editors, 8th International Conference on Computer Aided Verification, CAV'96, Rutgers (N.J.), 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Synchronous programming of reactive systems. Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4757-2231-4"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"D. Harel. Statecharts: A visual approach to complex systems. Science of Computer Programming, 8(3), 1987.","DOI":"10.1016\/0167-6423(87)90035-9"},{"issue":"9","key":"23_CR12","doi-asserted-by":"crossref","first-page":"1305","DOI":"10.1109\/5.97300","volume":"79","author":"N. Halbwachs","year":"1991","unstructured":"N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language Lustre. Proceedings of the IEEE, 79(9):1305\u20131320, September 1991.","journal-title":"Proceedings of the IEEE"},{"issue":"6\/7","key":"23_CR13","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1007\/BF01185559","volume":"29","author":"N. Halbwachs","year":"1992","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6\/7):523\u2013543, 1992.","journal-title":"Acta Informatica"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, F. Lagnier, and P. Raymond. Synchronous observers and the verification of reactive systems. In M. Nivat, C. Rattray, T. Rus, and G. Scollo, editors, Third Int. Conf. on Algebraic Methodology and Software Technology, AMAST'93, Twente, June 1993. Workshops in Computing, Springer Verlag.","DOI":"10.1007\/978-1-4471-3227-1_8"},{"key":"23_CR15","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K McMillan. A structural induction theorem for processes. In 8th ACM Symposium on Principles of Distributed Computing, pages 239\u2013247, Edmonton (Alberta), August 1989.","DOI":"10.1145\/72981.72998"},{"key":"23_CR16","unstructured":"D. Lesens. The boolean automaton network grammar checker home page. http:\/\/www.imag.fr\/VERIMAG\/PEOPLE\/David.Lesens\/BANG, 1997."},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In 24th ACM Symposium on Principles of Programming Languages, POPL'97, Paris, January 1997.","DOI":"10.1145\/263699.263747"},{"key":"23_CR18","series-title":"LNCS 630","volume-title":"CONCUR'92","author":"F. Maraninchi","year":"1992","unstructured":"F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. In CONCUR'92, Stony Brook, August 1992. LNCS 630, Springer Verlag."},{"key":"23_CR19","unstructured":"R. Marelly and O. Grumberg. Gormel-grammar oriented model checker. Technical report, The Technion, 1991."},{"key":"23_CR20","doi-asserted-by":"crossref","unstructured":"J. P. Queille and J. Sifakis. Specification and verification of concurrent systems in Cesar. In International Symposium on Programming. LNCS 137, Springer Verlag, April 1982.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, June 1989.","DOI":"10.1007\/3-540-52148-8_13"},{"key":"23_CR22","unstructured":"J. D. Ullman. Computational aspects of VLSI. Computer Science Press, 1984."},{"key":"23_CR23","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble. LNCS 407, Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T22:22:11Z","timestamp":1586470931000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000481"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540638889","9783540696612"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/bfb0000481","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}