{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:28:25Z","timestamp":1761596905924},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1994,2,1]],"date-time":"1994-02-01T00:00:00Z","timestamp":760060800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1994,2]]},"DOI":"10.1007\/bf01384084","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T03:30:17Z","timestamp":1112412617000},"page":"187-203","source":"Crossref","is-referenced-by-count":12,"title":["Model checking for action-based logics"],"prefix":"10.1007","volume":"4","author":[{"given":"Alessandro","family":"Fantechi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gioia","family":"Ristori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"CR1","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson, and J. Halpern. ?Sometime? and ?not never? revisited: On branching versus linear time temporal logic.Journal of ACM, 33(1): pp. 151?178, January 1986.","journal-title":"Journal of ACM"},{"issue":"1","key":"CR2","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency.Journal of ACM, 32, (1): 137?161, January, 1985.","journal-title":"Journal of ACM"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The anchored version of the temporal framework. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg (eds.).Lecture Notes in Computer Science, 354: 201?284, 1989.","DOI":"10.1007\/BFb0013024"},{"key":"CR4","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Gr\u00fcmberg. Characterizing finite Kripke structures in propositional temporal logic.Theoretical Computer, Science, 59: 115?131, 1988.","journal-title":"Theoretical Computer, Science"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and J. Srinivasan. Branching time temporal logic. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg (eds.)Lecture Notes in Computer Science, 354: 123?172, 1989.","DOI":"10.1007\/BFb0013022"},{"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":"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): 244?263, April 1986.","journal-title":"ACM TOPLAS"},{"key":"CR7","unstructured":"A. Boujani, S. Graf, and J. Sifakis: A logic for the description of behaviors and properties of concurrent systems. InLinear Time, Branching Time and Partial Order in Logics and Models for Concurrency, J. de Bakker, P. de Roever, and G. Rozenberg, (eds.).Lecture Notes in Computer Science 354: 398?410, 1989."},{"key":"CR8","unstructured":"C. Stirling. An introduction to modal and temporal logics for CCS. InConcurrency: Theory, Language, and Architecture, A. Yonezawa and T. Ito (eds.).Lecture Notes in Computer Science, 491: 2?20, 1990."},{"key":"CR9","first-page":"118","volume-title":"Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ?90) Philadelphia, PA, June, 1990","author":"R. Nicola De","year":"1990","unstructured":"R. De Nicola and F. Vaandrager. Three logics for branching bisimulations.Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ?90) Philadelphia, PA, June, 1990. IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 118?129. To appear also inJournal of ACM."},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"R. De Nicola and F. Vaandrager. Action versus state based logics for transition systems.Proceedings Ecole de Printemps on Semantics of Concurrency, April 1990, I. Guessarian (ed.).Lecture Notes in Computer Science, 469: 407?419, 1990.","DOI":"10.1007\/3-540-53479-2_17"},{"issue":"2","key":"CR11","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1016\/0304-3975(90)90038-J","volume":"72","author":"K.G. Larsen","year":"1990","unstructured":"K.G. Larsen. Proof systems for satisfiability in Hennessy-Milner logic with recursion.Theoretical Computer Science, 72(2): 265?288, 1990.","journal-title":"Theoretical Computer Science"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The concurrency workbench. InAutomatic Verification Methods for Finite State Systems, J. Sifakis (ed.).Lecture Notes in Computer Science, 407: 24?37, 1990.","DOI":"10.1007\/3-540-52148-8_3"},{"key":"CR13","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, and B. Steffen. A linear-time model checking algorithm, for the alternation free modal mu-calculus.Formal Methods in System Design, 2: 121?147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume":"104","author":"D. Park","year":"1981","unstructured":"D. Park. Concurrency and automata on infinite sequences.Proceedings 5th GI Conference. Lecture Notes in Computer Science 104: 167?183, 1981.","journal-title":"Proceedings 5th GI Conference. Lecture Notes in Computer Science"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"R. Milner. A calculus of communicating systems.Lecture Notes in Computer Science, 92, 1980.","DOI":"10.1007\/3-540-10235-3"},{"issue":"3","key":"CR16","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(83)90114-7","volume":"25","author":"R. Milner","year":"1983","unstructured":"R. Milner. Calculi for synchrony and asynchrony.Theoretical Computer Science, 25(3): 267?310, 1983.","journal-title":"Theoretical Computer Science"},{"key":"CR17","first-page":"613","volume-title":"Information Processing ?89","author":"R.J. Glabbeek van","year":"1989","unstructured":"R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. InInformation Processing ?89, G.X. Ritter (ed.). North Holland, Amsterdam, 1989, pp. 613?618."},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"B. Jonsson, A.H. Khan and J. Parrow. Implementing a model checking algorithm, by adapting existing automated tools. InAutomatic Verification Methods for Finite State Systems, J. Sifakis (ed.). Lecture Notes in Computer Science, 407: 179?188, 1990.","DOI":"10.1007\/3-540-52148-8_15"},{"key":"CR19","doi-asserted-by":"crossref","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, and G. Ristori. An action-based framework for verifying logical and behavioral properties of concurrent systems.Computer Networks and ISDN Systems, 25: 761?778, 1993.","journal-title":"Computer Networks and ISDN Systems"},{"key":"CR20","first-page":"428","volume-title":"Symbolic model checking: 1020 states and beyond","author":"J.R. Burch","year":"1990","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond.Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS ?90), Philadelphia, USA, June 1990 IEEE Computer Society Press, Los Alamitos, CA, 1990, pp. 428?439."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384084.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384084\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384084","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:24:58Z","timestamp":1586190298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994,2]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1994,2]]}},"alternative-id":["BF01384084"],"URL":"https:\/\/doi.org\/10.1007\/bf01384084","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994,2]]}}}