{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T13:46:24Z","timestamp":1742996784533,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319178219"},{"type":"electronic","value":"9783319178226"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17822-6_11","type":"book-chapter","created":{"date-parts":[[2015,4,22]],"date-time":"2015-04-22T05:57:31Z","timestamp":1429682251000},"page":"182-198","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Liveness Properties in CafeOBJ \u2013 A Case Study for Meta-Level Specifications"],"prefix":"10.1007","author":[{"given":"Norbert","family":"Preining","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kokichi","family":"Futatsugi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,4,23]]},"reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-08918-8_5","volume-title":"Rewriting and Typed Lambda Calculi","author":"K Bae","year":"2014","unstructured":"Bae, K., Meseguer, J.: Predicate abstraction of rewrite theories. In: Dowek, G. (ed.) RTA-TLCA 2014. LNCS, vol. 8560, pp. 61\u201376. Springer, Heidelberg (2014)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bae, K., Meseguer, J.: Infinite-state model checking of LTLR formulas unsing narrowing. In: WRLA 2014, 10th International Workshop on Rewriting Logic and its Applications, to appear","DOI":"10.1007\/978-3-319-12904-4_6"},{"issue":"3","key":"11_CR3","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1023\/A:1008700623084","volume":"16","author":"N Bj\u00f8rner","year":"2000","unstructured":"Bj\u00f8rner, N., Browne, A., Col\u00f3n, M., Finkbeiner, B., Manna, Z., Sipma, H., Uribe, T.E.: Verifying temporal properties of reactive systems: a step tutorial. Form. Methods Syst. Des. 16(3), 227\u2013270 (2000)","journal-title":"Form. Methods Syst. Des."},{"key":"11_CR4","volume-title":"Parallel Program Design\u2014A Foundation","author":"KM Chandy","year":"1989","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design\u2014A Foundation. Addison-Wesley, Boston (1989)"},{"issue":"1","key":"11_CR5","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/32.663997","volume":"24","author":"B Chetali","year":"1998","unstructured":"Chetali, B.: Formal verification of concurrent programs using the Larch prover. IEEE Trans. Softw. Eng. 24(1), 46\u201362 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"11_CR6","unstructured":"Futatsugi, K.: Generate and check methods for invariant verification in CafeOBJ. In: JAIST Research Report IS-RR-2013-006, http:\/\/hdl.handle.net\/10119\/11536 (2013)"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Futatsugi, K.: Generate and check method for verifying transition systems in CafeOBJ. Submitted for publication (2014)","DOI":"10.1007\/978-3-319-15545-6_13"},{"key":"11_CR8","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.tcs.2012.07.041","volume":"464","author":"K Futatsugi","year":"2012","unstructured":"Futatsugi, K., G\u00e2in\u00e2, D., Ogata, K.: Principles of proof scores in CafeOBJ. Theor. Comput. Sci. 464, 90\u2013112 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Lin., K.: Behavioral verification of distributed concurrent systems with BOBJ. In: QSIC, pp. 216\u2013235. IEEE Computer Society (2003)","DOI":"10.1109\/QSIC.2003.1319106"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-642-54624-2_26","volume-title":"Specification, Algebra, and Software","year":"2014","unstructured":"Iida, S., Meseguer, J., Ogata, K. (eds.): Specification, Algebra, and Software. LNCS, vol. 8373, pp. 520\u2013540. Springer, Heidelberg (2014)"},{"issue":"7\u20138","key":"11_CR11","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/j.jlap.2012.06.003","volume":"81","author":"J Meseguer","year":"2012","unstructured":"Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Log. Algebr. Program."},{"issue":"12","key":"11_CR12","doi-asserted-by":"publisher","first-page":"2985","DOI":"10.1093\/ietfec\/e90-a.12.2985","volume":"E90\u2013A","author":"K Ogata","year":"2007","unstructured":"Ogata, K., Futatsugi, K.: State machines as inductive types. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. E90\u2013A(12), 2985\u20132988 (2007)","journal-title":"IEICE Trans. Fundam. Electron. Commun. Comput. Sci."},{"issue":"12","key":"11_CR13","doi-asserted-by":"crossref","first-page":"2804","DOI":"10.1093\/ietisy\/e91-d.12.2804","volume":"91\u2013D","author":"K Ogata","year":"2008","unstructured":"Ogata, K., Futatsugi, K.: Proof score approach to verification of liveness properties. IEICE Trans. 91\u2013D(12), 2804\u20132817 (2008)","journal-title":"IEICE Trans."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-642-16901-4_33","volume-title":"Formal Methods and Software Engineering","author":"K Ogata","year":"2010","unstructured":"Ogata, K., Futatsugi, K.: A combination of forward and backward reachability analysis methods. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 501\u2013517. Springer, Heidelberg (2010)"},{"issue":"1","key":"11_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/343369.343370","volume":"1","author":"LC Paulson","year":"2000","unstructured":"Paulson, L.C.: Mechanizing UNITY in Isabelle. ACM Trans. Comput. Log. 1(1), 3\u201332 (2000)","journal-title":"ACM Trans. Comput. Log."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"11_CR17","unstructured":"Preining, N.: Specifications in CafeOBJ http:\/\/www.preining.info\/blog\/cafeobj\/"},{"key":"11_CR18","unstructured":"Preining, N., Futatsugi, K., Ogata, K.: Proving liveness properties using abstract state machines and $$n$$-visibility. In: Talk at the 22nd International Workshop on Algebraic Development Techniques WADT 2014, Sinaia, Romania, September 2014"},{"issue":"1","key":"11_CR19","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1016\/j.apal.2008.03.001","volume":"155","author":"V Rybakov","year":"2008","unstructured":"Rybakov, V.: Linear temporal logic with until and next, logical consecutions. Ann. Pure Appl. Log. 155(1), 32\u201345 (2008)","journal-title":"Ann. Pure Appl. Log."},{"issue":"5","key":"11_CR20","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1109\/90.731196","volume":"6","author":"D Stiliadis","year":"1998","unstructured":"Stiliadis, D., Varma, A.: Latency-rate servers: a general model for analysis of traffic scheduling algorithms. IEEE\/ACM Netw. 6(5), 611\u2013624 (1998)","journal-title":"IEEE\/ACM Netw."},{"issue":"1","key":"11_CR21","first-page":"39","volume":"16","author":"A Wierman","year":"2011","unstructured":"Wierman, A.: Fairness and scheduling in single server queues. Surv. Oper. Res. Manag. Sci. 16(1), 39\u201348 (2011)","journal-title":"Surv. Oper. Res. Manag. Sci."}],"container-title":["Lecture Notes in Computer Science","Logic-Based Program Synthesis and Transformation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17822-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,15]],"date-time":"2023-02-15T07:31:59Z","timestamp":1676446319000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17822-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319178219","9783319178226"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17822-6_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"23 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}