{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,25]],"date-time":"2022-04-25T16:27:51Z","timestamp":1650904071217},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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. Comput. Sci. Technol."],"published-print":{"date-parts":[[2016,1]]},"DOI":"10.1007\/s11390-016-1621-y","type":"journal-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T16:56:00Z","timestamp":1452185760000},"page":"198-216","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Game-Based Approach for PCTL* Stochastic Model Checking with Evidence"],"prefix":"10.1007","volume":"31","author":[{"given":"Yang","family":"Liu","sequence":"first","affiliation":[]},{"given":"Xuan-Dong","family":"Li","sequence":"additional","affiliation":[]},{"given":"Yan","family":"Ma","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,1,8]]},"reference":[{"key":"1621_CR1","doi-asserted-by":"crossref","unstructured":"Clarke E M, Emerson E A. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proc. the Workshop on Logic of Programs, May 1981, pp.52-71.","DOI":"10.1007\/BFb0025774"},{"key":"1621_CR2","doi-asserted-by":"crossref","unstructured":"Queille J P, Sifakis J. Specification and verification of concurrent systems in CESAR. In Proc. the 5th Colloquium on International Symposium on Programming, April 1982, pp.337-351.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"1621_CR3","unstructured":"Lin H M, ZhangWH. Model checking: Theories, techniques and applications. Acta Electronica Sinica, 2002, 30(12A): 1907\u20131912. (in Chinese)"},{"key":"1621_CR4","unstructured":"Baier C, Katoen J P. Principles of Model Checking. MIT Press, 2008."},{"key":"1621_CR5","doi-asserted-by":"crossref","unstructured":"Clarke E M, Emerson E A, Sifakis J. Model checking: Algorithmic verification and debugging. Communications of the ACM, 2009, 52(11): 74\u201384.","DOI":"10.1145\/1592761.1592781"},{"key":"1621_CR6","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D. Stochastic model checking. In Proc. the 7th International Conference on Formal Methods for Performance Evaluation, May 28-June 2, 2007, pp.220-270.","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"1621_CR7","doi-asserted-by":"crossref","unstructured":"Ndukwu U,Mclver A. An expectation transformer approach to predicate abstraction and data independence for probabilistic programs. In Proc. the 8th Workshop on Quantitative Aspects of Programming Languages, Mar. 2010, pp.129-143.","DOI":"10.4204\/EPTCS.28.9"},{"key":"1621_CR8","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort B R, Hermanns H, Katoen J P. Performance evaluation and model checking join forces. Communication of the ACM, 2010, 53(9): 74\u201385.","DOI":"10.1145\/1810891.1810912"},{"key":"1621_CR9","doi-asserted-by":"crossref","unstructured":"Duflot M, Kwiatkowska M, Norman G, Parker D, Peyronnet S, Picaronny C, Sproston J. Practical applications of probabilistic model checking to communication protocols. In Formal Methods for Industrial Critical Systems: A Survey of Applications, Gnesi S, Margaria T (eds.), John Wiley & Sons, Inc., 2012, pp.133-150","DOI":"10.1002\/9781118459898.ch7"},{"key":"1621_CR10","doi-asserted-by":"crossref","unstructured":"Calinescu R, Grunske L, Kwiatkowska M, Mirandola R, Tamburrelli G. Dynamic QoS management and optimisation in service-based systems. IEEE Transactions on Software Engineering, 2011, 37(3): 387\u2013409.","DOI":"10.1109\/TSE.2010.92"},{"key":"1621_CR11","unstructured":"Kwiatkowska M, Norman G, Parker D. Probabilistic model checking for systems biology. In Symbolic Systems Biology, Iyengar M S (ed.), Jones and Bartlett, 2010, pp.31-59."},{"key":"1621_CR12","doi-asserted-by":"crossref","unstructured":"Hansson H, Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing, 1994, 6(5): 512\u2013535.","DOI":"10.1007\/BF01211866"},{"key":"1621_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli A. The temporal logic of programs. In Proc. the 18th IEEE Symposium on Foundations of Computer Science, Oct.31-Nov.2, 1977, pp.46-67.","DOI":"10.1109\/SFCS.1977.32"},{"key":"1621_CR14","doi-asserted-by":"crossref","unstructured":"Aziz A, Sanwal K, Singhal V, Brayton R. Model-checking continuous time Markov chains. ACM Transactions on Computational Logic, 2000, 1(1): 162\u2013170.","DOI":"10.1145\/343369.343402"},{"key":"1621_CR15","doi-asserted-by":"crossref","unstructured":"Baier C, Haverkort B, Hermanns H, Katoen J P. Modelchecking algorithms for continuous-time Markov chains. IEEE Transactions on Software Engineering, 2003, 29(6): 524\u2013541.","DOI":"10.1109\/TSE.2003.1205180"},{"key":"1621_CR16","doi-asserted-by":"crossref","unstructured":"Liu Y, Miao H, Zeng H, Ma Y, Liu P. Nondeterministic probabilistic Petri net \u2014 A new method to studying qualitative and quantitative behaviors of system. Journal of Computer Science and Technology, 2013, 28(1): 203\u2013216.","DOI":"10.1007\/s11390-013-1323-7"},{"key":"1621_CR17","unstructured":"Hintikka J. Logic, Language-Games and Information: Kantian Themes in the Philosophy of Logic. Clarendon Press, Oxford, 1973."},{"key":"1621_CR18","doi-asserted-by":"crossref","unstructured":"Petri C A. Introduction to general net theory. In Lecture Notes in Computer Science 84, Brauer, W (ed.), Springer-Verlag, 1980, 84: 1\u201319.","DOI":"10.1007\/3-540-10001-6_21"},{"key":"1621_CR19","doi-asserted-by":"crossref","unstructured":"Bollig B, Leucker M, Weber M. Local parallel model checking for the alternation-free \u03bc-calculus. In Proc. the 9th International SPIN Workshop on Model Checking of Software, April 2002, pp.128-147.","DOI":"10.1007\/3-540-46017-9_11"},{"key":"1621_CR20","doi-asserted-by":"crossref","unstructured":"Savitch W J. Deterministic simulation of non-deterministic turing machines. In Proc. the 1st ACM Symposium on Theory of Computing, May 1969, pp.247-248.","DOI":"10.1145\/800169.805439"},{"key":"1621_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M, Norman G, Parker D. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. the 23rd International Conference on Computer Aided Verification, Jul. 2011, pp.585-591.","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"1621_CR22","doi-asserted-by":"crossref","unstructured":"Clarke E M, Jha S, Lu Y, Veith H. Tree-like counterexamples in model checking. In Proc. the 17th IEEE Symposium on Logic in Computer Science, Jul. 2002, pp.19-29.","DOI":"10.1109\/LICS.2002.1029814"},{"key":"1621_CR23","doi-asserted-by":"crossref","unstructured":"Chadha R, Viswanathan M. A counterexample-guided abstraction-refinement framework for Markov decision processes. ACM Transactions on Computational Logic, 2010, 12(1): 1:1\u20131:49.","DOI":"10.1145\/1838552.1838553"},{"key":"1621_CR24","unstructured":"Bonet P, Llado C M, Puijaner R, Knottenbelt W J. PIPE v2.5: A Petri net tool for performance modelling. In Proc. the 23rd Latin American Conference on Informatics (CLEI 2007), October 2007."},{"key":"1621_CR25","doi-asserted-by":"crossref","unstructured":"Dingle N J, Knottenbelt W J, Suto T. PIPE2: A tool for the performance evaluation of generalised stochastic Petri nets. ACM SIGMETRICS Performance Evaluation Review, 2009, 36(4): 34\u201339.","DOI":"10.1145\/1530873.1530881"},{"key":"1621_CR26","doi-asserted-by":"crossref","unstructured":"Ong C H L. Verification of higher-order computation: A game-semantic approach. In Proc. the 17th European Symposium on Programming, Mar.29-Apr.6, 2008, pp.299-306.","DOI":"10.1007\/978-3-540-78739-6_23"},{"key":"1621_CR27","doi-asserted-by":"crossref","unstructured":"Abramsky S, Ghica D, Murawski A, Ong C H L. Applying game semantics to compositional software modelling and verification. In Proc. the 10th International Conference Tools and Algorithms for the Construction and Analysis of Systems, Mar.29-Apr.2, 2004, pp.421-435.","DOI":"10.1007\/978-3-540-24730-2_32"},{"key":"1621_CR28","doi-asserted-by":"crossref","unstructured":"Abramsky S, Jagadeesan R. Game semantics for access control. Electronic Notes in Theoretical Computer Science, 2009, 249: 135\u2013156.","DOI":"10.1016\/j.entcs.2009.07.088"},{"key":"1621_CR29","doi-asserted-by":"crossref","unstructured":"Fredriksson O, Ghica D R. Abstract machines for game semantics, revisited. In Proc. the 28th Annual IEEE\/ACM Symposium Logic in Computer Science, Jun. 2013, pp.560-569.","DOI":"10.1109\/LICS.2013.63"},{"key":"1621_CR30","doi-asserted-by":"crossref","unstructured":"Stirling C. Proof systems for retracts in simply typed lambda calculus. In Proc. the 40th International Conference on Automata, Languages, and Programming, Jul. 2013, pp.398-409.","DOI":"10.1007\/978-3-642-39212-2_36"},{"key":"1621_CR31","doi-asserted-by":"crossref","unstructured":"Ghica D R. Applications of game semantics: From program analysis to hardware synthesis. In Proc. the 24th Annual IEEE Symposium on Logic in Computer Science, Aug. 2009, pp.17-26.","DOI":"10.1109\/LICS.2009.26"},{"key":"1621_CR32","unstructured":"Zhu X Y, Zhang W H, Li G Y, Lv Y, Lin H M. Report on advances in model checking. In Report on Advances in Computer Science and Technology (2011\u20132012), China Science and Technology Press, 2012. (in Chinese)"},{"key":"1621_CR33","unstructured":"Stirling C. Bisimulation, model checking and other games. http:\/\/homepages.inf.ed.ac.uk\/cps\/mathfit.pdf , Dec. 2015."},{"key":"1621_CR34","doi-asserted-by":"crossref","unstructured":"Stirling C. Modal and Temporal Properties of Processes. Springer-Verlag New York, 2001.","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"1621_CR35","doi-asserted-by":"crossref","unstructured":"Lange M, Stirling C. Model checking games for branching time logics. Journal of Logic Computation, 2002, 12(4): 623\u2013939.","DOI":"10.1093\/logcom\/12.4.623"},{"key":"1621_CR36","doi-asserted-by":"crossref","unstructured":"Shoham S, Grumberg O. Game-based framework for CTL counterexamples and 3-valued abstraction-refinement. ACM Transactions on Computational Logic (TOCL), 2007, 9(1): 1:1\u20131:52.","DOI":"10.1145\/1297658.1297659"},{"key":"1621_CR37","doi-asserted-by":"crossref","unstructured":"Fecher H, Huth M, Piterman N, Wagner D. PCTL model checking of Markov chains: Truth and falsity as winning strategies in games. Performance Evaluation, 2010, 67(9): 858\u2013872.","DOI":"10.1016\/j.peva.2009.07.002"},{"key":"1621_CR38","doi-asserted-by":"crossref","unstructured":"Tan L, Cleaveland R. Evidence-based model checking. In Proc. the 14th International Conference on Computer Aided Verification, Jul. 2002, pp.455-470.","DOI":"10.1007\/3-540-45657-0_37"},{"key":"1621_CR39","doi-asserted-by":"crossref","unstructured":"Namjoshi K. Certifying model checkers. In Proc. the 13th International Conference on Computer Aided Verification, Jul. 2001, pp.2-13.","DOI":"10.1007\/3-540-44585-4_2"},{"key":"1621_CR40","doi-asserted-by":"crossref","unstructured":"Peled D, Pnueli A, Zuck L. From falsification to verification. In Lecture Notes in Computer Science 2245, Hariharan R, Vinay V, Mukund M (eds.), Springer-Verlag, 2001, pp.292-304.","DOI":"10.1007\/3-540-45294-X_25"},{"key":"1621_CR41","doi-asserted-by":"crossref","unstructured":"Peled D, Zuck L. From model checking to a temporal proof. In Proc. the 8th International SPIN Workshop on Model Checking of Software, May 2001, pp.1-14.","DOI":"10.1007\/3-540-45139-0_1"},{"key":"1621_CR42","doi-asserted-by":"crossref","unstructured":"Han T T, Katoen J P, Damman B. Counterexample generation in probabilistic model checking. IEEE Transactions on Software Engineering, 2009, 35(2): 241\u2013257.","DOI":"10.1109\/TSE.2009.5"},{"key":"1621_CR43","doi-asserted-by":"crossref","unstructured":"Komuravelli A, P\u02d8as\u02d8areanu C S, Clarke E M. Assumeguarantee abstraction refinement for probabilistic systems. In Proc. the 24th International Conference on Computer Aided Verification, Jul. 2012, pp.310-326.","DOI":"10.1007\/978-3-642-31424-7_25"},{"key":"1621_CR44","unstructured":"Chatterjee K, Henzinger T, Jhala R, Majumdar R. Counter example-guided planning. In Proc. the 21st International Conference on Uncertainty in Artificial Intelligence, Jul. 2005, pp.104-111."},{"key":"1621_CR45","doi-asserted-by":"crossref","unstructured":"Hermanns H,Wachter B, Zhang L Z. Probabilistic CEGAR. In Proc. the 20th International Conference on Computer Aided Verification, Jul. 2008, pp.162-175.","DOI":"10.1007\/978-3-540-70545-1_16"},{"key":"1621_CR46","doi-asserted-by":"crossref","unstructured":"Aljazzar H, Leue S. Directed explicit state-space search in the generation of counterexamples for stochastic model checking. IEEE Transactions on Software Engineering, 2010, 36(1): 37\u201360.","DOI":"10.1109\/TSE.2009.57"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-016-1621-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-016-1621-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-016-1621-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,3]],"date-time":"2019-09-03T07:51:03Z","timestamp":1567497063000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-016-1621-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2016,1]]}},"alternative-id":["1621"],"URL":"https:\/\/doi.org\/10.1007\/s11390-016-1621-y","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1]]}}}