{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T12:02:48Z","timestamp":1702468968436},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2017,12,6]],"date-time":"2017-12-06T00:00:00Z","timestamp":1512518400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2018,5]]},"DOI":"10.1007\/s11432-017-9133-4","type":"journal-article","created":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T03:36:48Z","timestamp":1514345808000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Anti-chain based algorithms for timed\/probabilistic refinement checking"],"prefix":"10.1007","volume":"61","author":[{"given":"Ting","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tieming","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ye","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,6]]},"reference":[{"key":"9133_CR1","volume-title":"Model-Checking CSP","author":"A W Roscoe","year":"1994","unstructured":"Roscoe A W. Model-Checking CSP. Upper Saddle River: Prentice-Hall, 1994"},{"key":"9133_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J P. Principles of Model Checking. Cambridge: The MIT Press, 2008"},{"key":"9133_CR3","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/s11432-011-4530-2","volume":"55","author":"W Li","year":"2012","unstructured":"Li W, Li N. A formal semantics for program debugging. Sci China Inf Sci, 2012, 55: 133\u2013148","journal-title":"Sci China Inf Sci"},{"key":"9133_CR4","first-page":"128101","volume":"57","author":"H Li","year":"2014","unstructured":"Li H, Luo J, Li W. A formal semantics for debugging synchronous message passing-based concurrent programs. Sci China Inf Sci, 2014, 57: 128101","journal-title":"Sci China Inf Sci"},{"key":"9133_CR5","first-page":"032101","volume":"57","author":"X P Che","year":"2014","unstructured":"Che X P, Maag S. Testing protocols in internet of things by a formal passive technique. Sci China Inf Sci, 2014, 57: 032101","journal-title":"Sci China Inf Sci"},{"key":"9133_CR6","first-page":"413","volume-title":"The Origin of Concurrent Programming","author":"C A R Hoare","year":"1985","unstructured":"Hoare C A R. Communicating sequential processes. In: The Origin of Concurrent Programming. Berlin: Springer, 1985. 413\u2013443"},{"key":"9133_CR7","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1007\/s00165-005-0065-x","volume":"17","author":"A W Roscoe","year":"2005","unstructured":"Roscoe A W. On the expressive power of CSP refinement. Form Asp Comput, 2005, 17: 93\u2013112","journal-title":"Form Asp Comput"},{"key":"9133_CR8","first-page":"388","volume-title":"Model checking hierarchical probabilistic systems","author":"J Sun","year":"2010","unstructured":"Sun J, Song S, Liu Y. Model checking hierarchical probabilistic systems. In: Proceedings of the 12th International Conference on Formal Engineering Methods (ICFEM), Shanghai, 2010. 388\u2013403"},{"key":"9133_CR9","first-page":"98","volume-title":"Zone-based universality analysis for single-clock timed automata","author":"P A Abdulla","year":"2007","unstructured":"Abdulla P A, Ouaknine J, Quaas K, et al. Zone-based universality analysis for single-clock timed automata. In: Proceedings of International Conference on Fundamentals of Software Engineering (FSE), Luxembourg, 2007. 98\u2013112"},{"key":"9133_CR10","first-page":"43","volume-title":"When are timed automata determinizable","author":"C Baier","year":"2009","unstructured":"Baier C, Bertrand N, Bouyer P, et al. When are timed automata determinizable? In: Proceedings of International Colloquium on Automata, Languages, and Programming (ICALP), Rhodes, 2009. 43\u201354"},{"key":"9133_CR11","first-page":"54","volume-title":"On the language inclusion problem for timed automata: closing a decidability gap","author":"J Ouaknine","year":"2004","unstructured":"Ouaknine J, Worrell J. On the language inclusion problem for timed automata: closing a decidability gap. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LICS), Turku, 2004. 54\u201363"},{"key":"9133_CR12","first-page":"17","volume-title":"Antichains: a new algorithm for checking universality of finite automata","author":"M D Wulf","year":"2006","unstructured":"Wulf M D, Doyen L, Henzinger T A, et al. Antichains: a new algorithm for checking universality of finite automata. In: Proceedings of the 18th International Conference on Computer Aided Verification (CAV), Seattle, 2006. 17\u201330"},{"key":"9133_CR13","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"J Bengtsson","year":"2004","unstructured":"Bengtsson J, Yi W. Timed automata: semantics, algorithms and tools. In: Lectures on Concurrency and Petri Nets. Berlin: Springer, 2004. 87\u2013124"},{"key":"9133_CR14","first-page":"310","volume-title":"Are timed automata bad for a specification language? Language inclusion checking for timed automata","author":"T Wang","year":"2014","unstructured":"Wang T, Sun J, Liu Y, et al. Are timed automata bad for a specification language? Language inclusion checking for timed automata. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Grenoble, 2014. 310\u2013325"},{"key":"9133_CR15","first-page":"371","volume-title":"Developing model checkers using PAT","author":"Y Liu","year":"2010","unstructured":"Liu Y, Sun J, Dong J S. Developing model checkers using PAT. In: Proceedings of the 8th International Symposium on Automated Technology for Verification and Analysis (ATVA), Singapore, 2010. 371\u2013377"},{"key":"9133_CR16","first-page":"158","volume-title":"When simulation meets antichains","author":"P A Abdulla","year":"2010","unstructured":"Abdulla P A, Chen Y F, Holk L, et al. When simulation meets antichains. In: Proceedings of the 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Paphos, 2010. 158\u2013174"},{"key":"9133_CR17","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T A Henzinger","year":"1994","unstructured":"Henzinger T A, Nicollin X, Sifakis J, et al. Symbolic model checking for real-time systems. J Inform Comput, 1994, 111: 193\u2013244","journal-title":"J Inform Comput"},{"key":"9133_CR18","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1023\/B:FORM.0000026093.21513.31","volume":"24","author":"P Bouyer","year":"2004","unstructured":"Bouyer P. Forward analysis of updatable timed automata. Form Meth Syst Des, 2004, 24: 281\u2013320","journal-title":"Form Meth Syst Des"},{"key":"9133_CR19","volume-title":"Representing and modeling digital circuits","author":"T G Rokicki","year":"1993","unstructured":"Rokicki T G. Representing and modeling digital circuits. Dissertation for Ph.D. Degree. San Francisco: Stanford University, 1993"},{"key":"9133_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1507244.1507245","volume":"10","author":"S Tripakis","year":"2009","unstructured":"Tripakis S. Checking timed buchi automata emptiness on simulation graphs. ACM Trans Comput Logic, 2009, 10: 1\u201319","journal-title":"ACM Trans Comput Logic"},{"key":"9133_CR21","doi-asserted-by":"crossref","first-page":"204","DOI":"10.1007\/s10009-005-0190-0","volume":"8","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, Bouyer P, Larsen K G, et al. Lower and upper bounds in zonebased abstractions of timed automata. Int J Softw Tools Technol Trans, 2004, 8: 204\u2013215","journal-title":"Int J Softw Tools Technol Trans"},{"key":"9133_CR22","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M L Puterman","year":"1994","unstructured":"Puterman M L. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Hoboken: John Wiley and Sons, 1994"},{"key":"9133_CR23","volume-title":"Technical Report","author":"J J Vereijken","year":"1994","unstructured":"Vereijken J J. Fischer\u2019s Protocol in Timed Process Algebra. Technical Report. 1994"},{"key":"9133_CR24","first-page":"2","volume-title":"Timing-based mutual exclusion","author":"N Lynch","year":"1992","unstructured":"Lynch N, Shavit N. Timing-based mutual exclusion. In: Proceedings of Real-Time Systems Symposium (RTSS), Phoenix, 1992. 2\u201311"},{"key":"9133_CR25","first-page":"200","volume-title":"A tutorial on uppaal","author":"G Behrmann","year":"2004","unstructured":"Behrmann G, David R, Larsen K G. A tutorial on uppaal. In: Formal Methods for the Design of Real-Time Systems. Berlin: Springer, 2004. 200\u2013236"},{"key":"9133_CR26","first-page":"313","volume-title":"Model checking of real-time reachability properties using abstractions","author":"C Daws","year":"1998","unstructured":"Daws C, Tripakis S. Model checking of real-time reachability properties using abstractions. In: Proceedings of the 4th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Lisbon, 1998. 313\u2013329"},{"key":"9133_CR27","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/j.entcs.2005.04.012","volume":"128","author":"M Duflot","year":"2005","unstructured":"Duflot M, Fribourg L, Herault T, et al. Probabilistic model checking of the CSMA\/CD protocol using PRISM and APMC. Electron Notes Theor Comput Sci, 2005, 128: 195\u2013214","journal-title":"Electron Notes Theor Comput Sci"},{"key":"9133_CR28","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/j.entcs.2005.10.035","volume":"153","author":"V Gruhn","year":"2006","unstructured":"Gruhn V, Laue R. Patterns for timed property specifications. Electron Notes Theor Comput Sci, 2006, 153: 117\u2013133","journal-title":"Electron Notes Theor Comput Sci"},{"key":"9133_CR29","volume-title":"Systems Programming: Coping with Parallelism. Technical Report, IBM Almaden Research Center","author":"R K Treiber","year":"1986","unstructured":"Treiber R K. Systems Programming: Coping with Parallelism. Technical Report, IBM Almaden Research Center. 1986"},{"key":"9133_CR30","doi-asserted-by":"crossref","DOI":"10.1002\/0471478210","volume-title":"Distributed Computing: Fundamentals, Simulations, and Advanced Topics","author":"H Attiya","year":"2004","unstructured":"Attiya H, Welch J. Distributed Computing: Fundamentals, Simulations, and Advanced Topics. 2nd ed. Oxford: The Oxford University Press, 2004","edition":"2"},{"key":"9133_CR31","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-5(1:5)2009","volume":"5","author":"L Doyen","year":"2009","unstructured":"Doyen L, Raskin J F. Antichains for the automata-based approach to model checking. Logical Meth Comput Sci, 2009, 5: 1\u201320","journal-title":"Logical Meth Comput Sci"},{"key":"9133_CR32","first-page":"63","volume-title":"Antichains: alternative algorithms for LTL satisfiability and model-checking","author":"M D Wulf","year":"2008","unstructured":"Wulf M D, Doyen L, Maquet N, et al. Antichains: alternative algorithms for LTL satisfiability and model-checking. In: Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Budapest, 2008. 63\u201377"},{"key":"9133_CR33","first-page":"57","volume-title":"Antichain-based universality and inclusion testing over nondeterministic finite tree automata","author":"A Bouajjani","year":"2008","unstructured":"Bouajjani A, Habermehl P, Holk L, et al. Antichain-based universality and inclusion testing over nondeterministic finite tree automata. In: Proceedings of the 13th International Conference on Implementation and Application of Automata (CIAA), San Francisco, 2008. 57\u201367"},{"key":"9133_CR34","first-page":"263","volume-title":"An antichain algorithm for LTL realizability","author":"E Filiot","year":"2009","unstructured":"Filiot E, Jin N, Raskin J F. An antichain algorithm for LTL realizability. In: Proceedings of the 21st International Conference on Computer Aided Verification (CAV), Grenoble, 2009. 263\u2013277"},{"key":"9133_CR35","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur R, Dill D L. A theory of timed automata. Theory Comput Sci, 1994, 126: 183\u2013235","journal-title":"Theory Comput Sci"},{"key":"9133_CR36","first-page":"78","volume-title":"Timed automata with integer resets: language inclusion and expressiveness","author":"P V Suman","year":"2008","unstructured":"Suman P V, Pandya P K, Krishna S N, et al. Timed automata with integer resets: language inclusion and expressiveness. In: Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Saint-Malo, 2008. 78\u201392"},{"key":"9133_CR37","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/S0304-3975(97)00173-4","volume":"211","author":"R Alur","year":"1999","unstructured":"Alur R, Fix L, Henzinger T A. Event-clock automata: a determinizable class of timed automata. Theor Comput Sci, 1999, 211: 253\u2013273","journal-title":"Theor Comput Sci"},{"key":"9133_CR38","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K G Larsen","year":"1997","unstructured":"Larsen K G, Petterson P, Wang Y. UPPAAL in a nutshell. J Softw Tools Technol Trans, 1997, 1: 134\u2013152","journal-title":"J Softw Tools Technol Trans"},{"key":"9133_CR39","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine S. Kronos: a verification tool for real-time systems. J Softw Tools Technol Trans, 1997, 1: 123\u2013133","journal-title":"J Softw Tools Technol Trans"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9133-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-017-9133-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-017-9133-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T03:36:57Z","timestamp":1514345817000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-017-9133-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,6]]},"references-count":39,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,5]]}},"alternative-id":["9133"],"URL":"https:\/\/doi.org\/10.1007\/s11432-017-9133-4","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,6]]},"article-number":"052105"}}