{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T21:42:55Z","timestamp":1770327775894,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540664628","type":"print"},{"value":"9783540482574","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48257-1_14","type":"book-chapter","created":{"date-parts":[[2007,7,20]],"date-time":"2007-07-20T20:25:09Z","timestamp":1184963109000},"page":"228-242","source":"Crossref","is-referenced-by-count":10,"title":["A Symbolic Model Checker for ACTL"],"prefix":"10.1007","author":[{"given":"A.","family":"Fantechi","sequence":"first","affiliation":[]},{"given":"S.","family":"Gnesi","sequence":"additional","affiliation":[]},{"given":"F.","family":"Mazzanti","sequence":"additional","affiliation":[]},{"given":"R.","family":"Pugliese","sequence":"additional","affiliation":[]},{"given":"E.","family":"Tronci","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"D. Austry, G. Boudol. Algebre de processus et synchronization, Theoretical Computer Science, 1(30), 1984.","DOI":"10.1016\/0304-3975(84)90067-7"},{"key":"14_CR2","unstructured":"C. Bernardeschi, A. Fantechi, S. Gnesi. Formal Specification and Verification of the Inter-Channel Consistency Network, GUARDS Esprit project, Technical Report D3A4\/6004c, 1997."},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1023\/A:1008645826258","volume":"12","author":"C. Bernardeschi","year":"1998","unstructured":"C. Bernardeschi, A. Fantechi, S. Gnesi, S. Larosa, G. Mongardi, D. Romano. A Formal Verification Environment for Railway Signaling System Design, in Formal Methods in System Design 12, 139\u2013161, 1998.","journal-title":"Formal Methods in System Design"},{"key":"14_CR4","first-page":"207","volume":"54","author":"A. Bouali","year":"1994","unstructured":"A. Bouali, S. Gnesi, S. Larosa. The integration Project for the JACK Environment, Bulletin of the EATCS, n.54, pp.207\u2013223, 1994. (see also http:\/\/repl.iei.pi.cnr.it\/projects\/JACK .)","journal-title":"Bulletin of the EATCS"},{"key":"14_CR5","unstructured":"R.S. Boyer, J.S., Moore. \u201cA Computational Logic\u201d, ACM Monograph Series, Academic Press, 1979."},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"R.E. Bryant. Graph Based algorithms for boolean function manipulation, IEEE Transaction on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"14_CR7","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D. Dill, J. Hwang. Symbolic Model Checking 1020 states and beyond, in Proceedings of LICS, 1990."},{"issue":"2","key":"14_CR8","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P., \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specification,\u201d ACM Transaction on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"14_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-52148-8_3","volume-title":"Proc. of Automatic Verification Methods for Finite State Systems","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland, J. Parrow, B. Steffen. The Concurrency Workbench, in Proc. of Automatic Verification Methods for Finite State Systems, LNCS 407, pp. 24\u201337, 1990."},{"key":"14_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/3-540-61474-5_87","volume-title":"Proc. of Computer Aided Verification","author":"R. Cleaveland","year":"1996","unstructured":"R. Cleaveland, S. Sims. The NCSU Concurrency Workbench, in Proc. of Computer Aided Verification, LNCS 1102, pp. 394\u2013397, 1996."},{"issue":"7","key":"14_CR11","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1016\/0169-7552(93)90047-8","volume":"25","author":"R. Nicola De","year":"1993","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. An action-based framework for verifying logical and behavioural properties of concurrent systems, Computer Networks and ISDN Systems, 25(7):761\u2013778, 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"14_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/3-540-60385-9_15","volume-title":"Proceedings of CHARME\u2019 95","author":"R. Nicola De","year":"1995","unstructured":"R. De Nicola, A. Fantechi, S. Gnesi, G. Ristori. Verifying Hardware Components within JACK, in Proceedings of CHARME\u2019 95, LNCS 987, pp. 246\u2013260, 1995."},{"key":"14_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Proceedings Ecole de Printemps on Semantics of Concurrency","author":"R. Nicola De","year":"1990","unstructured":"R. De Nicola, F. W. Vaandrager. Action versus State based Logics for Transition Systems, Proceedings Ecole de Printemps on Semantics of Concurrency, LNCS 469, pp. 407\u2013419, 1990."},{"key":"14_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson, J. Halpern. \u201cSometime\u201d and \u201cNot never\u201d revisited: On branching versus linear time temporal logic, JACM 33:151\u2013178, 1986.","journal-title":"JACM"},{"key":"14_CR15","unstructured":"E.A. Emerson, C. Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus, in Proceedings of LICS, pp. 267\u2013278, 1986."},{"key":"14_CR16","unstructured":"A. Fantechi, S. Gnesi, G. Ristori. From ACTL to \u03bc-Calculus, ERCIM Workshop on Theory and Practice in Verification, Pisa, December 9\u201311, 1992."},{"key":"14_CR17","series-title":"Lect Notes Comput Sci","first-page":"436","volume-title":"CAV\u201996","author":"J.C. Fernandez","year":"1996","unstructured":"J.C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, M. Sighireanu. CADP: A Protocol Validation and Verification Toolbox, CAV\u201996, LNCS 1102, pp. 436\u2013440, 1996."},{"key":"14_CR18","unstructured":"G. Ferro. \u201cAMC: ACTL Model Checker. Reference Manual\u201d, IEI-Internal Report B4-47, December 1994."},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy, R. Milner. Algebraic Laws for Nondeterminism and Concurrency, JACM 32:137\u2013161, 1985.","journal-title":"JACM"},{"key":"14_CR20","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the Propositional \u03bc-calculus, Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"14_CR21","unstructured":"E. Madelaine, R. de Simone. The FC2 Reference Manual, Available by ftp from http:\/\/cma.cma.fr:pub\/verif as file http:\/\/fc2refman.ps.gz , 1993."},{"key":"14_CR22","unstructured":"R. Milner. Communication and Concurrency, Prentice-Hall International, Englewood Cliffs, 1989."},{"key":"14_CR23","series-title":"Technical Report","volume-title":"A Structural Approach to Operational Semantics","author":"G.D. Plotkin","year":"1981","unstructured":"G.D. Plotkin. A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, Aarhus University, Dep. of Computer Science, Denmark, 1981."},{"key":"14_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/3-540-60973-3_100","volume-title":"FME\u225096","author":"R. Pugliese","year":"1996","unstructured":"R. Pugliese, E. Tronci. Automatic Verification of a Hydroelectric Power Plant. FME\u225096, LNCS 1051, pp. 425\u2013444, 1996."},{"key":"14_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BFb0023720","volume-title":"Proceedings of the Workshop on Computer Aided Verification","author":"V. Roy","year":"1990","unstructured":"V. Roy, R. De Simone. AUTO and Autograph, in Proceedings of the Workshop on Computer Aided Verification, LNCS 531, 65\u201375, 1990."},{"key":"14_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Concurrency: Theory, Language, and Architecture","author":"C. Stirling","year":"1989","unstructured":"C. Stirling. An Introduction to modal and temporal logics for CCS, In Concurrency: Theory, Language, and Architecture, LNCS 391, 1989."},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"E. Tronci. Hardware Verification, Boolean Logic Programming, Boolean Functional Programming, in Proceedings of LICS, 1995.","DOI":"10.1109\/LICS.1995.523275"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"E. Tronci. On Computing Optimal Controllers for Finite State Systems, Proc. of the 36th IEEE Conf. on Decision and Control, 1997.","DOI":"10.1109\/CDC.1997.652410"}],"container-title":["Lecture Notes in Computer Science","Applied Formal Methods \u2014 FM-Trends 98"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48257-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T11:08:00Z","timestamp":1556708880000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48257-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664628","9783540482574"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-48257-1_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[1999]]}}}