{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T01:52:27Z","timestamp":1761961947370,"version":"build-2065373602"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642163098"},{"type":"electronic","value":"9783642163104"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-16310-4_14","type":"book-chapter","created":{"date-parts":[[2010,10,1]],"date-time":"2010-10-01T03:44:29Z","timestamp":1285904669000},"page":"208-225","source":"Crossref","is-referenced-by-count":10,"title":["The Linear Temporal Logic of Rewriting Maude Model Checker"],"prefix":"10.1007","author":[{"given":"Kyungmin","family":"Bae","sequence":"first","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/3-540-49059-0_15","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"P. Abdulla","year":"1999","unstructured":"Abdulla, P., Annichini, A., Bouajjani, A.: Symbolic verification of lossy channel systems: Application to the bounded retransmission protocol. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 208\u2013222. Springer, Heidelberg (1999)"},{"key":"14_CR2","series-title":"ENTCS","volume-title":"Proc. 9th Inte. Workshop on Rule-Based Programming","author":"K. Bae","year":"2008","unstructured":"Bae, K., Meseguer, J.: A rewriting-based model checker for the temporal logic of rewriting. In: Proc. 9th Inte. Workshop on Rule-Based Programming. ENTCS, Elsevier, Amsterdam (2008)"},{"key":"14_CR3","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2007","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2007)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-540-79707-4_11","volume-title":"Formal Methods for Industrial Critical Systems","author":"M.H. Beek ter","year":"2008","unstructured":"ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action\/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 133\u2013148. Springer, Heidelberg (2008)"},{"key":"14_CR5","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":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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., 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":"14_CR7","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":"14_CR8","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":"14_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"E.M. Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2001)"},{"key":"14_CR10","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":"14_CR11","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":"14_CR12","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2006.07.002","volume":"66","author":"F. Dur\u00e1n","year":"2007","unstructured":"Dur\u00e1n, F., Meseguer, J.: Maude\u2019s module algebra. Science of Computer Programming\u00a066, 125\u2013153 (2007)","journal-title":"Science of Computer Programming"},{"key":"14_CR13","series-title":"ENTCS","volume-title":"Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications","author":"S. Eker","year":"2002","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker. In: Gadducci, F., Montanari, U. (eds.) Proc. 4th. Intl. Workshop on Rewriting Logic and its Applications. ENTCS. Elsevier, Amsterdam (2002)"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-44829-2_16","volume-title":"Model Checking Software","author":"S. Eker","year":"2003","unstructured":"Eker, S., Meseguer, J., Sridharanarayanan, A.: The Maude LTL model checker and its implementation. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 230\u2013234. Springer, Heidelberg (2003)"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-540-78743-3_17","volume-title":"Fundamental Approaches to Software Engineering","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: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol.\u00a04961, pp. 230\u2013245. Springer, Heidelberg (2008)"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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)"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-44585-4_6","volume-title":"Computer Aided Verification","author":"P. Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast ltl to b\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 53\u201365. Springer, Heidelberg (2001)"},{"key":"14_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), \n                    \n                      http:\/\/fmt.isti.cnr.it\/WEBPAPER\/gmaica2005.pdf"},{"issue":"1","key":"14_CR19","doi-asserted-by":"publisher","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":"14_CR20","first-page":"23","volume-title":"The Spin Verification System","author":"G. Holzmann","year":"1996","unstructured":"Holzmann, G., Peled, D., Yannakakis, M.: On nested depth first search (extended abstract). In: The Spin Verification System, pp. 23\u201332. American Mathematical Society, Providence (1996)"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"14_CR22","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":"14_CR23","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. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"14_CR24","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":"14_CR25","doi-asserted-by":"publisher","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)"},{"issue":"3","key":"14_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."},{"key":"14_CR27","unstructured":"Meseguer, J.: The temporal logic of rewriting. Tech. Rep. UIUCDCS-R-2007-2815, CS Dept., University of Illinois at Urbana-Champaign (February 2007) (revised) (November 2007)"},{"issue":"1","key":"14_CR28","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":"14_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-540-68679-8_22","volume-title":"Concurrency, Graphs and Models","author":"J. Meseguer","year":"2008","unstructured":"Meseguer, J.: The temporal logic of rewriting: A gentle introduction. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol.\u00a05065, pp. 354\u2013382. Springer, Heidelberg (2008)"},{"key":"14_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-45085-6_2","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, pp. 2\u201316. Springer, Heidelberg (2003)"},{"key":"14_CR31","doi-asserted-by":"publisher","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":"14_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"14_CR33","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":"14_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/10722167_21","volume-title":"Computer Aided Verification","author":"F. Somenzi","year":"2000","unstructured":"Somenzi, F., Bloem, R.: Efficient b\u00fcchi automata from ltl formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 248\u2013263. Springer, Heidelberg (2000)"},{"key":"14_CR35","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","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16310-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T12:06:34Z","timestamp":1553169994000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16310-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642163098","9783642163104"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16310-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}