{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,3,24]],"date-time":"2023-03-24T11:29:10Z","timestamp":1679657350607},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,7,30]],"date-time":"2014-07-30T00:00:00Z","timestamp":1406678400000},"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":["J Comb Optim"],"published-print":{"date-parts":[[2016,2]]},"DOI":"10.1007\/s10878-014-9776-3","type":"journal-article","created":{"date-parts":[[2014,7,29]],"date-time":"2014-07-29T06:07:55Z","timestamp":1406614075000},"page":"577-603","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Verifying safety critical task scheduling systems in PPTL axiom system"],"prefix":"10.1007","volume":"31","author":[{"given":"Nan","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mengfei","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bin","family":"Gu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhenhua","family":"Duan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cong","family":"Tian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,7,30]]},"reference":[{"key":"9776_CR1","doi-asserted-by":"crossref","unstructured":"Bertot Y, Cast\u00e9ran P (2004) Interactive theorem proving and program development. Springer-Verlag, Berlin, Heidelberg","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9776_CR2","doi-asserted-by":"crossref","unstructured":"Brock B, Kaufmann M, Moore J (1996) Acl2 theorems about commercial microprocessors. In: Srivas M, Camilleri A (eds) Proceedings of the 1st international conference on formal methods in computer-aided design. Springer-Verlag, London, pp 275\u2013293","DOI":"10.1007\/BFb0031816"},{"key":"9776_CR3","volume-title":"Temporal logic and temporal logic programming","author":"Z Duan","year":"2005","unstructured":"Duan Z (2005) Temporal logic and temporal logic programming. Science Press, Beijing"},{"key":"9776_CR4","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1016\/j.tcs.2012.01.026","volume":"497","author":"Z Duan","year":"2013","unstructured":"Duan Z, Zhang N, Koutny M (2013) A complete proof system for propositional projection temporal logic. Theoret Comput Sci 497:84\u2013107","journal-title":"Theoret Comput Sci"},{"key":"9776_CR5","unstructured":"Gordon M, Melham T (1993) Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge"},{"issue":"5","key":"9776_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann G (1997) The model checker spin. IEEE Trans Softw Eng 23(5):279\u2013295","journal-title":"IEEE Trans Softw Eng"},{"key":"9776_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking: an approach to the state explosion problem","author":"K McMillan","year":"1993","unstructured":"McMillan K (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer Academic, Dordrecht"},{"key":"9776_CR8","doi-asserted-by":"crossref","unstructured":"Owre S, Rushby J (1992) Pvs: a prototype verification system. In: Kapur D (ed) Proceedings of the 11th international conference on automated deduction. Springer-Verlag, Heidelberg, pp 748\u2013752","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9776_CR9","volume-title":"Isabelle\u2014a generic theorem prover","author":"L Paulson","year":"1994","unstructured":"Paulson L (1994) Isabelle\u2014a generic theorem prover. Springer, Berlin"},{"key":"9776_CR10","unstructured":"Sistla A (1983) Theoretical issues in the design and verification of distributed systems. PhD thesis, Harvard University"},{"issue":"1","key":"9776_CR11","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1017\/S096012950800738X","volume":"19","author":"C Tian","year":"2009","unstructured":"Tian C, Duan Z (2009) Complexity of propositional projection temporal logic with star. Math Str Comput Sci 19(1):73\u2013100","journal-title":"Math Str Comput Sci"},{"key":"9776_CR12","doi-asserted-by":"crossref","unstructured":"Vardi M (1988) A temporal fixpoint calculus. In: POPL \u201988 Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. ACM, New York, pp 250\u2013259","DOI":"10.1145\/73560.73582"},{"key":"9776_CR13","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper P (1983) Temporal logic can be more expressive. Info Control 56:72\u201399","journal-title":"Info Control"}],"container-title":["Journal of Combinatorial Optimization"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-014-9776-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10878-014-9776-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10878-014-9776-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T04:23:24Z","timestamp":1559276604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10878-014-9776-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,30]]},"references-count":13,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,2]]}},"alternative-id":["9776"],"URL":"https:\/\/doi.org\/10.1007\/s10878-014-9776-3","relation":{},"ISSN":["1382-6905","1573-2886"],"issn-type":[{"value":"1382-6905","type":"print"},{"value":"1573-2886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7,30]]}}}