{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,20]],"date-time":"2025-04-20T04:19:51Z","timestamp":1745122791833,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642342806"},{"type":"electronic","value":"9783642342813"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34281-3_28","type":"book-chapter","created":{"date-parts":[[2012,10,29]],"date-time":"2012-10-29T18:38:09Z","timestamp":1351535889000},"page":"398-413","source":"Crossref","is-referenced-by-count":5,"title":["Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization"],"prefix":"10.1007","author":[{"given":"Truong Khanh","family":"Nguyen","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":[]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"publisher","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. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Taubenfeld, G.: Results about Fast Mutual Exclusion. In: IEEE Real-Time Systems Symposium, pp. 12\u201322 (1992)","DOI":"10.1109\/REAL.1992.242680"},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-540-45069-6_13","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2003","unstructured":"Beyer, D., Lewerentz, C., Noack, A.: Rabbit: A Tool for BDD-Based Verification of Real-Time Systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 122\u2013125. Springer, Heidelberg (2003)"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing Assumptions and Verification of Finite-State Concurrent Systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"T.A. Henzinger","year":"1992","unstructured":"Henzinger, T.A., Manna, Z., Pnueli, A.: What Good Are Digital Clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"key":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-642-14295-6_15","volume-title":"Computer Aided Verification","author":"F. Herbreteau","year":"2010","unstructured":"Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed B\u00fcchi Automata. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 148\u2013161. Springer, Heidelberg (2010)"},{"key":"28_CR7","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall (1985)"},{"key":"28_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0055036","volume-title":"Automata, Languages and Programming","author":"Y. Kesten","year":"1998","unstructured":"Kesten, Y., Pnueli, A., Raviv, L.-O.: Algorithmic Verification of Linear Temporal Logic Specifications. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 1\u201316. Springer, Heidelberg (1998)"},{"issue":"1","key":"28_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/7351.7352","volume":"5","author":"L. Lamport","year":"1987","unstructured":"Lamport, L.: A Fast Mutual Exclusion Algorithm. ACM Trans. Comput. Syst.\u00a05(1), 1\u201311 (1987)","journal-title":"ACM Trans. Comput. Syst."},{"key":"28_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11560548_14","volume-title":"Correct Hardware Design and Verification Methods","author":"L. Lamport","year":"2005","unstructured":"Lamport, L.: Real-Time Model Checking Is Really Simple. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 162\u2013175. Springer, Heidelberg (2005)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Lynch, N.A., Shavit, N.: Timing-Based Mutual Exclusion. In: IEEE Real-Time Systems Symposium, pp. 2\u201311 (1992)","DOI":"10.1109\/REAL.1992.242681"},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/S1567-8326(02)00023-1","volume":"52-53","author":"J.B. M\u00f8ller","year":"2002","unstructured":"M\u00f8ller, J.B., Hulgaard, H., Andersen, H.R.: Symbolic Model Checking of Timed Guarded Commands Using Difference Decision Diagrams. J. Log. Algebr. Program.\u00a052-53, 53\u201377 (2002)","journal-title":"J. Log. Algebr. Program."},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y.: BDD-based Discrete Analysis of Timed Systems (2012), http:\/\/www.comp.nus.edu.sg\/%7Epat\/bddlib","DOI":"10.1007\/978-3-642-32759-9_28"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-32759-9_28","volume-title":"FM 2012: Formal Methods","author":"T.K. Nguyen","year":"2012","unstructured":"Nguyen, T.K., Sun, J., Liu, Y., Dong, J.S., Liu, Y.: Improved BDD-Based Discrete Analysis of Timed Systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol.\u00a07436, pp. 326\u2013340. Springer, Heidelberg (2012)"},{"key":"28_CR15","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Worrell, J.: Timed CSP = Closed Timed Safety Automata. Electrical Notes Theoretical Computer Science 68(2) (2002)","DOI":"10.1016\/S1571-0661(05)80369-X"},{"key":"28_CR16","unstructured":"Palikareva, H., Ouaknine, J., Roscoe, B.: Faster FDR Counterexample Generation Using SAT-Solving. ECEASST 23 (2009)"},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-60630-0_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A.W. Roscoe","year":"1995","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical Compression for Model-Checking CSP or How to Check 1020 Dining Philosophers for Deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 133\u2013152. Springer, Heidelberg (1995)"},{"key":"28_CR18","unstructured":"Schneider, S.: Concurrent and Real-Time Systems: The CSP Approach. Wiley (2000)"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., Andr\u00e9, E.: Modeling and Verifying Hierarchical Real-time Systems using Stateful Timed CSP. TOSEM (to appear, 2012)","DOI":"10.1145\/2430536.2430537"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: Towards Flexible Verification under Fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 709\u2013714. Springer, Heidelberg (2009)"},{"key":"28_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-642-10373-5_30","volume-title":"Formal Methods and Software Engineering","author":"J. Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Zhang, X.: Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol.\u00a05885, pp. 581\u2013600. Springer, Heidelberg (2009)"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying Progress in Timed Systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol.\u00a01601, pp. 299\u2013314. Springer, Heidelberg (1999)"},{"key":"28_CR23","unstructured":"Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS, pp. 332\u2013344. IEEE Computer Society (1986)"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Wang, F.: Symbolic Verification of Complex Real-Time Systems with Clock-Restriction Diagram. In: FORTE, pp. 235\u2013250 (2001)","DOI":"10.1007\/0-306-47003-9_15"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34281-3_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,19]],"date-time":"2025-04-19T21:24:33Z","timestamp":1745097873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34281-3_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642342806","9783642342813"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34281-3_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}