{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T13:12:17Z","timestamp":1791033137320,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540686767","type":"print"},{"value":"9783540686798","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-68679-8_22","type":"book-chapter","created":{"date-parts":[[2008,6,10]],"date-time":"2008-06-10T02:58:16Z","timestamp":1213066696000},"page":"354-382","source":"Crossref","is-referenced-by-count":25,"title":["The Temporal Logic of Rewriting: A Gentle Introduction"],"prefix":"10.1007","author":[{"given":"Jos\u00e9","family":"Meseguer","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-88733-1","volume-title":"Proc. FMICS","author":"M. Beek","year":"2008","unstructured":"Beek, M., Fantechi, A., Gnesi, S., Mazzanti, F.: An action\/state-based model-checking approach for the analysis of communication protocols for Service-Oriented Applications. In: Proc. FMICS. LNCS, Springer, Heidelberg (to appear, 2008)"},{"key":"22_CR2","volume-title":"Handbook of Modal Logic","author":"J. Bradfield","year":"2006","unstructured":"Bradfield, J., Stirling, C.: Modal Mu-Calculi. In: Handbook of Modal Logic, vol.\u00a03, Elsevier, Amsterdam (2006)"},{"issue":"1-3","key":"22_CR3","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1016\/j.tcs.2006.04.012","volume":"360","author":"R. Bruni","year":"2006","unstructured":"Bruni, R., Meseguer, J.: Semantic foundations for generalized rewrite theories. Theor. Comput. Sci.\u00a0360(1-3), 386\u2013414 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-540-24727-2_7","volume-title":"Foundations of Software Science and Computation Structures","author":"L. Caires","year":"2004","unstructured":"Caires, L.: Behavioral and spatial observations in a logic for the pi-calculus. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 72\u201387. Springer, Heidelberg (2004)"},{"issue":"2","key":"22_CR5","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/S0890-5401(03)00137-8","volume":"186","author":"L. Caires","year":"2003","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Inf. Comput.\u00a0186(2), 194\u2013235 (2003)","journal-title":"Inf. Comput."},{"issue":"3","key":"22_CR6","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1016\/j.tcs.2003.10.041","volume":"322","author":"L. Caires","year":"2004","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency - II. Theor. Comput. Sci.\u00a0322(3), 517\u2013565 (2004)","journal-title":"Theor. Comput. Sci."},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/11589976_5","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Grumberg, O., Ouaknine, J., Sharygina, N., Touili, T., Veith, H.: State\/event software verification for branching-time specifications. In: Romijn, J.M.T., Smith, G.P., van de Pol, J. (eds.) IFM 2005. LNCS, vol.\u00a03771, pp. 53\u201369. Springer, Heidelberg (2005)"},{"key":"22_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Integrated Formal Methods","author":"S. Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol.\u00a02999, pp. 128\u2013147. Springer, Heidelberg (2004)"},{"key":"22_CR9","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s00165-005-0071-z","volume":"17","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N., Sinha, N.: Concurrent software verification with states, events, and deadlocks. Formal Aspects of Computing\u00a017, 461\u2013483 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"22_CR10","volume-title":"Parallel Program Design: A Foundation","author":"K.M. Chandy","year":"1988","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)"},{"key":"22_CR11","volume-title":"Model Checking","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Meseguer, J., Lincoln, P., Mart\u00ed-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"22_CR13","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/978-3-540-78743-3_17","volume-title":"Proc. FASE 2008","author":"A. Fantechi","year":"2008","unstructured":"Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A model checking approach for verifying COWS specifications. In: FASE 2008. LNCS, vol.\u00a04961, pp. 230\u2013245. Springer, Heidelberg (2008)"},{"key":"22_CR15","unstructured":"Fantechi, A., Gnesi, S., Ristori, G.: From ACTL to Mu-Calculus. In: Proc. ERCIM Workshop on Theory and Practice of Verification (Pisa, Italy, December 1992), pp. 3\u201310. IEI-CNR (1992)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"438","DOI":"10.1007\/978-3-540-44616-3_25","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Fiadeiro","year":"2000","unstructured":"Fiadeiro, J., Mart\u00ed-Oliet, N., Maibaum, T., Meseguer, J., Pita, I.: Towards a verification logic for rewriting logic. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol.\u00a01827, pp. 438\u2013458. Springer, Heidelberg (2000)"},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci.\u00a018(2), 194\u2013211 (1979)","journal-title":"J. Comput. Syst. Sci."},{"key":"22_CR18","unstructured":"Gnesi, S., Mazzanti, F.: A Model Checking Verification Environment for UML Statecharts. In: Proceedings XLIII AICA Annual Conference, University of Udine - AICA 2005, October 2-5 (2005)"},{"issue":"1","key":"22_CR19","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery\u00a032(1), 137\u2013172 (1985)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"22_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-45309-1_11","volume-title":"Programming Languages and Systems","author":"M. Huth","year":"2001","unstructured":"Huth, M., Jagadeesan, R., Schmidt, D.: Modal transition systems: A foundation for three-valued program analysis. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 155\u2013169. Springer, Heidelberg (2001)"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/3-540-69108-1_20","volume-title":"Application and Theory of Petri Nets 1998","author":"E. Kindler","year":"1998","unstructured":"Kindler, E., Vesper, T.: ESTL: A temporal logic for events and states. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol.\u00a01420, pp. 365\u2013384. Springer, Heidelberg (1998)"},{"key":"22_CR22","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci.\u00a027, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"22_CR23","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"Lamport, L.: A temporal logic of actions. ACM Trans. on Prog. Lang. and Systems\u00a016(3), 872\u2013923 (1994)","journal-title":"ACM Trans. on Prog. Lang. and Systems"},{"key":"22_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0931-7","volume-title":"The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification","author":"Z. Manna","year":"1992","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems \u2013 Specification. Springer, Heidelberg (1992)"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/S0304-3975(01)00357-7","volume":"285","author":"N. Mart\u00ed-Oliet","year":"2002","unstructured":"Mart\u00ed-Oliet, N., Meseguer, J.: Rewriting logic: roadmap and bibliography. Theoretical Computer Science\u00a0285, 121\u2013154 (2002)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"22_CR26","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1093\/logcom\/exi015","volume":"15","author":"N. Mart\u00ed-Oliet","year":"2005","unstructured":"Mart\u00ed-Oliet, N., Pita, I., Fiadeiro, J.L., Meseguer, J., Maibaum, T.S.E.: A verification logic for rewriting logic. J. Log. Comput.\u00a015(3), 317\u2013352 (2005)","journal-title":"J. Log. Comput."},{"issue":"4","key":"22_CR27","doi-asserted-by":"publisher","first-page":"461","DOI":"10.3166\/tsi.22.461-495","volume":"22","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R.: Logiques temporelles bas\u00e9es sur actions pour la v\u00e9rification des syst\u00e8mes asynchrones. Technique et Science Informatiques\u00a022(4), 461\u2013495 (2003); also, INRIA Report 5032 (December 2003)","journal-title":"Technique et Science Informatiques"},{"issue":"6","key":"22_CR28","doi-asserted-by":"crossref","first-page":"893","DOI":"10.3233\/JCS-2004-12604","volume":"12","author":"C. Meadows","year":"2004","unstructured":"Meadows, C., Syverson, P.F., Cervesato, I.: Formal specification and analysis of the group domain of interpretation protocol using NPATRL and the NRL protocol analyzer. Journal of Computer Security\u00a012(6), 893\u2013931 (2004)","journal-title":"Journal of Computer Security"},{"key":"22_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/978-3-540-32033-3_19","volume-title":"Term Rewriting and Applications","author":"J. Meseguer","year":"2005","unstructured":"Meseguer, J.: Localized fairness: A rewriting semantics. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 250\u2013263. Springer, Heidelberg (2005)"},{"issue":"1","key":"22_CR30","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"22_CR31","unstructured":"Meseguer, J.: The temporal logic of rewriting. Technical Report UIUCDCS-R-2007-2815, CS Dept., University of Illinois at Urbana-Champaign (February 2007)"},{"key":"22_CR32","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-19","author":"J. Meseguer","year":"2003","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, Springer, Heidelberg (2003)"},{"key":"22_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-8528-6","volume-title":"A Discipline of Multiprogramming","author":"J. Misra","year":"2001","unstructured":"Misra, J.: A Discipline of Multiprogramming. Springer, Heidelberg (2001)"},{"key":"22_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R.D. Nicola","year":"1990","unstructured":"Nicola, R.D., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol.\u00a0469, pp. 407\u2013419. Springer, Heidelberg (1990)"},{"key":"22_CR35","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/j.entcs.2004.06.026","volume":"117","author":"M. Palomino","year":"2005","unstructured":"Palomino, M., Pita, I.: Proving VLRL action properties with the Maude model checker. Electr. Notes Theor. Comput. Sci.\u00a0117, 113\u2013133 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"22_CR36","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-74128-2_8","volume-title":"Model Checking and Artificial Intelligence","author":"C. Pecheur","year":"2007","unstructured":"Pecheur, C., Raimondi, F.: Symbolic model checking of logics with actions. In: Edelkamp, S., Lomuscio, A. (eds.) MoChArt IV. LNCS (LNAI), vol.\u00a04428, pp. 113\u2013128. Springer, Heidelberg (2007)"},{"key":"22_CR37","first-page":"109","volume-title":"FOCS 1976","author":"V.R. Pratt","year":"1976","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: FOCS 1976, pp. 109\u2013121. IEEE Computer Society Press, Los Alamitos (1976)"},{"key":"22_CR38","series-title":"ENTCS","volume-title":"Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications","author":"P. Thati","year":"2002","unstructured":"Thati, P., Sen, K., Mart\u00ed-Oliet, N.: An executable specification of asynchronous Pi-Calculus semantics and may testing in Maude 2.0. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS, Elsevier, Amsterdam (2002)"},{"key":"22_CR39","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1016\/S0304-3975(01)00366-8","volume":"285","author":"P. Viry","year":"2002","unstructured":"Viry, P.: Equational rules for rewriting logic. Theoretical Computer Science\u00a0285, 487\u2013517 (2002)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Concurrency, Graphs and Models"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68679-8_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,2]],"date-time":"2019-03-02T03:21:54Z","timestamp":1551496914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68679-8_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540686767","9783540686798"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68679-8_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}