{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T04:39:39Z","timestamp":1742963979274,"version":"3.40.3"},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319266251"},{"type":"electronic","value":"9783319266268"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-26626-8_35","type":"book-chapter","created":{"date-parts":[[2015,12,9]],"date-time":"2015-12-09T04:08:43Z","timestamp":1449634123000},"page":"481-495","source":"Crossref","is-referenced-by-count":1,"title":["Symbolic Model Checking for Alternating Projection Temporal Logic"],"prefix":"10.1007","author":[{"given":"Haiyang","family":"Wang","sequence":"first","affiliation":[]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,12,9]]},"reference":[{"key":"35_CR1","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"35_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"35_CR3","volume-title":"Concepts, Algorithms, and Tools for Model Checking","author":"JP Katoen","year":"1999","unstructured":"Katoen, J.P.: Concepts, Algorithms, and Tools for Model Checking. IMMD, Erlangen (1999)"},{"key":"35_CR4","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of 18th IEEE Symposium Foundation of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"35_CR5","unstructured":"Wang, H., Xu, Q.: Temporal logics over infinite intervals. Technical report 158, UNU\/IIST, Macau (1999)"},{"key":"35_CR6","unstructured":"Cau, A., Moszkowski, B., Zedan, H.: Interval Temporal Logic (2006). \n                      http:\/\/www.cms.dmu.ac.uk\/~cau\/itlhomepage\/itlhomepage.html"},{"key":"35_CR7","volume-title":"Temporal Logic and Temporal Logic Programming","author":"Z Duan","year":"2005","unstructured":"Duan, Z.: Temporal Logic and Temporal Logic Programming. Science Press, Beijing (2005)"},{"key":"35_CR8","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"694","DOI":"10.1007\/978-3-642-16901-4_45","volume-title":"Formal Methods and Software Engineering","author":"C Tian","year":"2010","unstructured":"Tian, C., Duan, Z.: Alternating interval based temporal logics. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 694\u2013709. Springer, Heidelberg (2010)"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-12896-4_374","volume-title":"Logics of Programs","author":"B Moszkowski","year":"1984","unstructured":"Moszkowski, B., Manna, Z., Kozen, D.: Reasoning in interval temporal logic. In: Clarke, E., Kozen, D. (eds.) Logics of Programs. LNCS, vol. 164, pp. 371\u2013382. Springer, Heidelberg (1984)"},{"key":"35_CR11","unstructured":"Moszkowski, B.: A complete axiom system for propositional interval temporal logic with infinite time. ArXiv Prepr (2012). \n                      ArXiv1207.3816"},{"key":"35_CR12","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/s00236-007-0062-z","volume":"45","author":"Z Duan","year":"2008","unstructured":"Duan, Z., Tian, C., Zhang, L.: A decision procedure for propositional projection temporal logic with infinite models. Acta Inform. 45, 43\u201378 (2008)","journal-title":"Acta Inform."},{"key":"35_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/3-540-58216-9_48","volume-title":"Logic Programming and Automated Reasoning","author":"Z Duan","year":"1994","unstructured":"Duan, Z., Koutny, M., Holt, C.: Projection in temporal logic programming. In: Pfenning, F. (ed.) LPAR 1994. LNCS, vol. 822, pp. 333\u2013344. Springer, Heidelberg (1994)"},{"key":"35_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S., Rajamani, R.K., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"key":"35_CR16","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., et al.: Symbolic model checking: \n                      \n                        \n                      \n                      $$10^{20}$$\n                      \n                        \n                          \n                            10\n                            20\n                          \n                        \n                      \n                     states and beyond. In: Proceedings of Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 428\u2013439. IEEE (1990)"},{"key":"35_CR17","doi-asserted-by":"crossref","unstructured":"Pang, T., Duan, Z., Tian, C.: Symbolic model checking for propositional projection temporal logic. In: Sixth International Symposium on Theoretical Aspects of Software Engineering (TASE 2012). IEEE, pp. 9\u201316 (2012)","DOI":"10.1109\/TASE.2012.35"},{"key":"35_CR18","doi-asserted-by":"crossref","unstructured":"Lomuscio, A., Raimondi, F.: Model checking knowledge, strategies, and games in multi-agent systems. In: Proceedings of the Fifth International Joint Conference on Autonomous Agents and Multiagent Systems, pp. 161\u2013168. ACM (2006)","DOI":"10.1145\/1160633.1160660"},{"key":"35_CR19","volume-title":"Reasoning About Knowledge","author":"JY Halpern","year":"1995","unstructured":"Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)"},{"issue":"8","key":"35_CR20","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"100","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 100(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."}],"container-title":["Lecture Notes in Computer Science","Combinatorial Optimization and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26626-8_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T17:03:50Z","timestamp":1559322230000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26626-8_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319266251","9783319266268"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26626-8_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}