{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,16]],"date-time":"2026-01-16T07:43:26Z","timestamp":1768549406570,"version":"3.49.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,12,13]],"date-time":"2013-12-13T00:00:00Z","timestamp":1386892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Front. Comput. Sci."],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s11704-013-3091-5","type":"journal-article","created":{"date-parts":[[2013,12,13]],"date-time":"2013-12-13T02:08:27Z","timestamp":1386900507000},"page":"1-16","source":"Crossref","is-referenced-by-count":38,"title":["Model checking with fairness assumptions using PAT"],"prefix":"10.1007","volume":"8","author":[{"given":"Yuanjie","family":"Si","sequence":"first","affiliation":[]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Jun","family":"Pang","sequence":"additional","affiliation":[]},{"given":"Shao Jie","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Xiaohu","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,13]]},"reference":[{"key":"3091_CR1","first-page":"511","volume-title":"Proceedings of the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering","author":"D Giannakopoulou","year":"1999","unstructured":"Giannakopoulou D, Magee J, Kramer J. Checking progress with action priority: is it fair? In: Proceedings of the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering. 1999, 511\u2013527"},{"issue":"2","key":"3091_CR2","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport L. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, 1977, 3(2): 125\u2013143","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3091_CR3","doi-asserted-by":"crossref","DOI":"10.1515\/9781400864041","volume-title":"Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R P Kurshan","year":"1995","unstructured":"Kurshan R P. Computer-aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, 1995"},{"key":"3091_CR4","first-page":"318","volume-title":"Proceedings of the 10th International Conference on Formal Engineering Methods","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong J S, Wang H H. Specifying and verifying event-based fairness enhanced systems. In: Proceedings of the 10th International Conference on Formal Engineering Methods. 2008, 318\u2013337"},{"key":"3091_CR5","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-05089-3_9","volume-title":"FM 2009: Formal Methods","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Roychoudhury A, Liu S, Dong J. Fair model checking with process counter abstraction. FM 2009: Formal Methods, 2009, 123\u2013139"},{"key":"3091_CR6","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/11945529_28","volume-title":"Proceedings of the 10th International Conference on Principles of Distributed Systems","author":"M J Fischer","year":"2006","unstructured":"Fischer M J, Jiang H. Self-stabilizing leader election in networks of finite-state anonymous agents. In: Proceedings of the 10th International Conference on Principles of Distributed Systems. 2006, 395\u2013409"},{"key":"3091_CR7","first-page":"103","volume-title":"Proceedings of the 9th International Conference on Principles of Distributed Systems","author":"D Angluin","year":"2005","unstructured":"Angluin D, Aspnes J, Fischer M J, Jiang H. Self-stabilizing population protocols. In: Proceedings of the 9th International Conference on Principles of Distributed Systems. 2005, 103\u2013117"},{"key":"3091_CR8","first-page":"37","volume-title":"Proceedings of the 2006 International Conference on Distributed Computing in Sensor Systems","author":"D Angluin","year":"2006","unstructured":"Angluin D, Fischer M J, Jiang H. Stabilizing consensus in mobile networks. In: Proceedings of the 2006 International Conference on Distributed Computing in Sensor Systems. 2006, 37\u201350"},{"key":"3091_CR9","volume-title":"Computing Research Repository","author":"D Canepa","year":"2008","unstructured":"Canepa D, Potop-Butucaru M. Stabilizing Token Schemes for Population Protocols. Computing Research Repository, 2008, abs\/0806.3471"},{"key":"3091_CR10","first-page":"149","volume-title":"Proceedings of the 14th International SPIN Workshop","author":"K Y Rozier","year":"2007","unstructured":"Rozier K Y, Vardi M Y. LTL Satisfiability Checking. In: Proceedings of the 14th International SPIN Workshop. 2007, 149\u2013167"},{"key":"3091_CR11","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-540-31980-1_13","volume-title":"Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"M Hammer","year":"2005","unstructured":"Hammer M, Knapp A, Merz S. Truly on-the-fly LTL model checking. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 191\u2013205"},{"key":"3091_CR12","first-page":"185","volume-title":"Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"J Pang","year":"2008","unstructured":"Pang J, Luo Z Q, Deng Y X. On automatic verification of self-stabilizing population protocols. In: Proceedings of the 2nd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2008, 185\u2013192"},{"key":"3091_CR13","volume-title":"Distributed Systems of Simple Interacting Agents","author":"H Jiang","year":"2007","unstructured":"Jiang H. Distributed Systems of Simple Interacting Agents. PhD thesis, Yale University, 2007"},{"key":"3091_CR14","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1109\/TASE.2009.32","volume-title":"Proceedings of the third IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Dong J S, Chen C Q. Integrating specification and programs for system modeling and verification. In: Proceedings of the third IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 127\u2013135"},{"key":"3091_CR15","volume-title":"International Series on Computer Science","author":"C A R Hoare","year":"1985","unstructured":"Hoare C A R. Communicating Sequential Processes. International Series on Computer Science. Prentice-Hall, 1985"},{"key":"3091_CR16","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-540-24756-2_8","volume-title":"Proceedings of the 4th International Conference on Integrated Formal Methods","author":"S Chaki","year":"2004","unstructured":"Chaki S, Clarke E M, Ouaknine J, Sharygina N, Sinha N. State\/event-based software model checking. In: Proceedings of the 4th International Conference on Integrated Formal Methods. 2004, 128\u2013147"},{"key":"3091_CR17","doi-asserted-by":"crossref","first-page":"264","DOI":"10.1007\/3-540-10843-2_22","volume-title":"Proceedings of the 8th Colloquium on Automata, Languages and Programming","author":"D J Lehmann","year":"1981","unstructured":"Lehmann D J, Pnueli A, Stavi J. Impartiality, justice and fairness: the ethics of concurrent termination. In: Proceedings of the 8th Colloquium on Automata, Languages and Programming. 1981, 264\u2013277"},{"key":"3091_CR18","volume-title":"The SPINModel Checker: Primer and Reference Manual","author":"G J Holzmann","year":"2003","unstructured":"Holzmann G J. The SPINModel Checker: Primer and Reference Manual. Addison Wesley, 2003"},{"issue":"4","key":"3091_CR19","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/PL00008921","volume":"13","author":"L Lamport","year":"2000","unstructured":"Lamport L. Fairness and hyperfairness. Distributed Computing, 2000, 13(4): 239\u2013245","journal-title":"Distributed Computing"},{"key":"3091_CR20","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/978-3-540-78163-9_21","volume-title":"Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation","author":"A Pnueli","year":"2008","unstructured":"Pnueli A, Sa\u2019ar Y. All you need is compassion. In: Proceedings of the 9th International Conference on Verification, Model Checking and Abstract Interpretation. 2008, 233\u2013247"},{"issue":"1","key":"3091_CR21","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.tcs.2005.07.004","volume":"345","author":"J Geldenhuys","year":"2005","unstructured":"Geldenhuys J, Valmari A. More efficient on-the-fly LTL verification with Tarjan\u2019s algorithm. Theoritical Computer Science, 2005, 345(1): 60\u201382","journal-title":"Theoritical Computer Science"},{"key":"3091_CR22","first-page":"16","volume-title":"Proceedings of the 5th Scandinavian Workshop on Algorithm Theory","author":"M R Henzinger","year":"1996","unstructured":"Henzinger M R, Telle J A. Faster algorithms for the nonemptiness of streett automata and for communication protocol pruning. In: Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. 1996, 16\u201327"},{"issue":"1","key":"3091_CR23","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/s10703-006-4342-y","volume":"28","author":"Y Kesten","year":"2006","unstructured":"Kesten Y, Pnueli A, Raviv L, Shahar E. Model checking with strong fairness. Formal Methods and System Design, 2006, 28(1): 57\u201384","journal-title":"Formal Methods and System Design"},{"key":"3091_CR24","doi-asserted-by":"crossref","first-page":"362","DOI":"10.1145\/1375581.1375625","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation","author":"M Musuvathi","year":"2008","unstructured":"Musuvathi M, Qadeer S. Fair stateless model checking. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation. 2008, 362\u2013371"},{"key":"3091_CR25","volume-title":"Principles ofModel Checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J. Principles ofModel Checking. TheMIT Press, 2008"},{"key":"3091_CR26","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1007\/978-3-540-31980-1_12","volume-title":"Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"S Schwoon","year":"2005","unstructured":"Schwoon S, Esparza J. A note on on-the-fly verification algorithms. In: Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. 2005, 174\u2013190"},{"key":"3091_CR27","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"2","author":"R Tarjan","year":"1972","unstructured":"Tarjan R. Depth-first search and linear graph algorithms. SIAMJournal on Computing, 1972, 2: 146\u2013160","journal-title":"SIAMJournal on Computing"},{"key":"3091_CR28","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1109\/TASE.2009.51","volume-title":"Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering","author":"Y Liu","year":"2009","unstructured":"Liu Y, Pang J, Sun J, Zhao J. Verification of population ring protocols in pat. In: Proceedings of the 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering. 2009, 81\u201389"},{"issue":"3","key":"3091_CR29","doi-asserted-by":"crossref","first-page":"94","DOI":"10.1145\/945526.945527","volume":"34","author":"K Alagarsamy","year":"2003","unstructured":"Alagarsamy K. Some myths about famous mutual exclusion algorithms. SIGACT News, 2003, 34(3): 94\u2013103","journal-title":"SIGACT News"},{"key":"3091_CR30","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume":"5643","author":"J Sun","year":"2009","unstructured":"Sun J, Liu Y, Dong J S, Pang J. PAT: towards flexible verification under fairness. Lecture Notes in Computer Science, 2009, 5643: 709\u2013714","journal-title":"Lecture Notes in Computer Science"},{"issue":"4","key":"3091_CR31","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1007\/BF01872848","volume":"2","author":"K R Apt","year":"1988","unstructured":"Apt K R, Francez N, Katz S. Appraising fairness in languages for distributed programming. Distributed Computing, 1988, 2(4): 226\u2013241","journal-title":"Distributed Computing"},{"key":"3091_CR32","volume-title":"Fairness. Texts and Monographs in Computer Science","author":"N Francez","year":"1986","unstructured":"Francez N. Fairness. Texts and Monographs in Computer Science. Springer-Verlag, 1986"},{"issue":"4","key":"3091_CR33","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/BF02242712","volume":"6","author":"P C Attie","year":"1993","unstructured":"Attie P C, Francez N, Grumberg O. Fairness and hyperfairness in multi-party interactions. Distributed Computing, 1993, 6(4): 245\u2013254","journal-title":"Distributed Computing"},{"key":"3091_CR34","first-page":"195","volume":"19","author":"J P Queille","year":"1983","unstructured":"Queille J P, Sifakis J. Fairness and related properties in transition systems-a temporal logic to deal with fairness. Acta Informaticae, 1983, 19: 195\u2013220","journal-title":"Acta Informaticae"},{"issue":"3","key":"3091_CR35","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/BF01887206","volume":"1","author":"M Z Kwiatkowska","year":"1989","unstructured":"Kwiatkowska M Z. Event fairness and non-interleaving concurrency. Formal Aspects of Computing, 1989, 1(3): 213\u2013228","journal-title":"Formal Aspects of Computing"},{"key":"3091_CR36","first-page":"458","volume-title":"Proceedings of the 16th International Conference on Concurrency Theory","author":"H V\u00f6lzer","year":"2005","unstructured":"V\u00f6lzer H, Varacca D, Kindler E. Defining fairness. In: Proceedings of the 16th International Conference on Concurrency Theory. 2005, 458\u2013472"},{"issue":"1-4","key":"3091_CR37","doi-asserted-by":"crossref","first-page":"175","DOI":"10.3233\/FI-2000-43123409","volume":"43","author":"T Latvala","year":"2000","unstructured":"Latvala T, Heljanko K. Coping with strong fairness. Fundamenta Informaticae, 2000, 43(1-4): 175\u2013193","journal-title":"Fundamenta Informaticae"},{"issue":"2\/3","key":"3091_CR38","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Vardi M Y, Wolper P, Yannakakis M. Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1992, 1(2\/3): 275\u2013288","journal-title":"Memory-efficient algorithms for the verification of temporal properties. Formal Methods in System Design"},{"key":"3091_CR39","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1007\/978-3-642-21437-0_32","volume-title":"FM 2011: Formal Methods","author":"S Zhang","year":"2011","unstructured":"Zhang S, Sun J, Pang J, Liu Y, Dong J. On combining state space reductions with global fairness assumptions. FM 2011: Formal Methods, 2011, 432\u2013447"},{"key":"3091_CR40","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/318593.318622","volume-title":"Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages","author":"O Lichtenstein","year":"1985","unstructured":"Lichtenstein O, Pnueli A. Checking that finite state concurrent programs satisfy their linear specification. In: Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1985, 97\u2013107"},{"issue":"3","key":"3091_CR41","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E A Emerson","year":"1987","unstructured":"Emerson E A, Lei C L. Modalities for model checking: branching time logic strikes back. Science of Computer Programming, 1987, 8(3): 275\u2013306","journal-title":"Science of Computer Programming"},{"issue":"2","key":"3091_CR42","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1023\/A:1008727508722","volume":"18","author":"R H Hardin","year":"2001","unstructured":"Hardin R H, Kurshan R P, Shukla S K, Vardi M Y. A new heuristic for bad cycle detection using BDDs. Formal Methods in System Design, 2001, 18(2): 131\u2013140","journal-title":"Formal Methods in System Design"},{"key":"3091_CR43","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/3-540-63166-6_13","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification","author":"N Klarlund","year":"1997","unstructured":"Klarlund N. An n log n Algorithm for Online BDD Refinement. In: Proceedings of the 9th International Conference on Computer Aided Verification. 1997, 107\u2013118"},{"key":"3091_CR44","first-page":"226","volume-title":"Proceedings of the 8th International Conference on Formal Engineering Methods","author":"J S Dong","year":"2006","unstructured":"Dong J S, Liu Y, Sun J, Zhang X. Verification of computation orchestration via timed automata. In: Proceedings of the 8th International Conference on Formal Engineering Methods. 2006, 226\u2013245"},{"key":"3091_CR45","first-page":"342","volume-title":"Proceedings of the 8th International Conference on Formal Engineering Methods","author":"J S Dong","year":"2006","unstructured":"Dong J S, Hao P, Sun J, Zhang X. A reasoning method for timed CSP based on constraint solving. In: Proceedings of the 8th International Conference on Formal Engineering Methods. 2006, 342\u2013359"},{"key":"3091_CR46","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun J, Liu Y, Dong J S. Model checking csp revisited: introducing a process analysis toolkit. In: Proceedings of the 3rd International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. 2008, 307\u2013322"}],"container-title":["Frontiers of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-3091-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11704-013-3091-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11704-013-3091-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,12]],"date-time":"2020-08-12T01:24:06Z","timestamp":1597195446000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11704-013-3091-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,13]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["3091"],"URL":"https:\/\/doi.org\/10.1007\/s11704-013-3091-5","relation":{},"ISSN":["2095-2228","2095-2236"],"issn-type":[{"value":"2095-2228","type":"print"},{"value":"2095-2236","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,13]]}}}