{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:03:24Z","timestamp":1743138204392,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":23,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819606160"},{"type":"electronic","value":"9789819606177"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_20","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T14:47:40Z","timestamp":1732805260000},"page":"353-374","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Tableau-Based Approach to\u00a0Model Checking Linear Temporal Properties"],"prefix":"10.1007","author":[{"given":"Canh","family":"Minh Do","sequence":"first","affiliation":[]},{"given":"Tsubasa","family":"Takagi","sequence":"additional","affiliation":[]},{"given":"Kazuhiro","family":"Ogata","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"issue":"1","key":"20_CR1","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/71.80120","volume":"1","author":"TE Anderson","year":"1990","unstructured":"Anderson, T.E.: The performance of spin lock alternatives for shared-memory multiprocessors. IEEE Trans. Parallel Distrib. Syst. 1(1), 6\u201316 (1990)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Aung, M.N., Phyo, Y., Do, C.M., Ogata, K.: A divide and conquer approach to eventual model checking. Mathematics 9(4) (2021)","DOI":"10.3390\/math9040368"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Aung, M.N., Phyo, Y., Do, C.M., Ogata, K.: A tool for model checking eventual model checking in a stratified way. In: 9th DSA, pp. 270\u2013279 (2022)","DOI":"10.1109\/DSA56465.2022.00045"},{"key":"20_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-4129-7","volume-title":"Mathematical Logic for Computer Science","author":"M Ben-Ari","year":"2012","unstructured":"Ben-Ari, M.: Mathematical Logic for Computer Science. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-1-4471-4129-7"},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"issue":"5","key":"20_CR6","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"EM Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512\u20131542 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"3","key":"20_CR7","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s100090050035","volume":"2","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Minea, M., Peled, D.A.: State space reduction using partial order techniques. Int. J. Softw. Tools Technol. Transf. 2(3), 279\u2013287 (1999)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_CR8","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-10575-8_9","volume-title":"Handbook of Model Checking","author":"J Marques-Silva","year":"2018","unstructured":"Marques-Silva, J., Malik, S.: Propositional SAT solving. In: Handbook of Model Checking, pp. 247\u2013275. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_9"},{"key":"20_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71999-1","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71999-1"},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"Do, C.M., Phyo, Y., Ogata, K.: A divide & conquer approach to until and until stable model checking. In: 34th SEKE (2022)","DOI":"10.18293\/SEKE2022-058"},{"key":"20_CR11","doi-asserted-by":"publisher","first-page":"133749","DOI":"10.1109\/ACCESS.2022.3230844","volume":"10","author":"CM Do","year":"2022","unstructured":"Do, C.M., Phyo, Y., Ogata, K.: Sequential and parallel tools for model checking conditional stable properties in a layered way. IEEE Access 10, 133749\u2013133765 (2022)","journal-title":"IEEE Access"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Do, C.M., Phyo, Y., Riesco, A., Ogata, K.: Optimization techniques for model checking leads-to properties in a stratified way. ACM Trans. Softw. Eng. Methodol. 32(6) (2023)","DOI":"10.1145\/3604610"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Do, C.M., Phyo, Y., Riesco, A., Ogata, K.: A parallel stratified model checking technique\/tool for leads-to properties. In: 7th ISSSR, pp. 155\u2013166 (2021)","DOI":"10.1109\/ISSSR53171.2021.00011"},{"key":"20_CR14","series-title":"IFIP Advances in Information and Communication Technology","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-0-387-34892-6_1","volume-title":"Protocol Specification, Testing and Verification XV","author":"R Gerth","year":"1996","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV 1995. IAICT, pp. 3\u201318. Springer, Boston, MA (1996). https:\/\/doi.org\/10.1007\/978-0-387-34892-6_1"},{"issue":"7\u20138","key":"20_CR15","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. Algebraic Methods Program. 81(7\u20138), 721\u2013781 (2012)","journal-title":"J. Log. Algebraic Methods Program."},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L de Moura","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: from refutation to verification. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14\u201326. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_2"},{"issue":"7","key":"20_CR17","doi-asserted-by":"publisher","first-page":"384","DOI":"10.3390\/info14070384","volume":"14","author":"Y Phyo","year":"2023","unstructured":"Phyo, Y., Aung, M.N., Do, C.M., Ogata, K.: A layered and parallelized method of eventual model checking. Information 14(7), 384 (2023)","journal-title":"Information"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-030-85315-0_7","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2021","author":"Y Phyo","year":"2021","unstructured":"Phyo, Y., Do, C.M., Ogata, K.: A divide & conquer approach to conditional stable model checking. In: Cerone, A., \u00d6lveczky, P.C. (eds.) ICTAC 2021. LNCS, vol. 12819, pp. 105\u2013111. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85315-0_7"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"1353","DOI":"10.1093\/comjnl\/bxaa183","volume":"65","author":"Y Phyo","year":"2021","unstructured":"Phyo, Y., Do, C.M., Ogata, K.: A divide & conquer approach to leads-to model checking. Comput. J. 65, 1353\u20131364 (2021)","journal-title":"Comput. J."},{"key":"20_CR20","doi-asserted-by":"crossref","unstructured":"Phyo, Y., Do, C.M., Ogata, K.: A support tool for the L+1-layer divide & conquer approach to leads-to model checking. In: COMPSAC, pp. 854\u2013863. IEEE (2021)","DOI":"10.1109\/COMPSAC51774.2021.00118"},{"key":"20_CR21","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2013.07.007","volume":"296","author":"F van der Berg","year":"2013","unstructured":"van der Berg, F., Laarman, A.: SpinS: extending LTSmin with Promela through SpinJa. Electron. Notes Theor. Comput. Sci. 296, 95\u2013105 (2013)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"MY Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol. 1043, pp. 238\u2013266. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-60915-6_6"},{"issue":"110\/111","key":"20_CR23","first-page":"119","volume":"28","author":"P Wolper","year":"1985","unstructured":"Wolper, P.: The tableau method for temporal logic: an overview. Logique et Anal. (N.S.) 28(110\/111), 119\u2013136 (1985)","journal-title":"Logique et Anal. (N.S.)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:09:53Z","timestamp":1732806593000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}