{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T10:42:11Z","timestamp":1740134531263,"version":"3.37.3"},"reference-count":14,"publisher":"Wiley","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/3.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61373034","61170304","2011DFG13000","KZ201210028036"],"award-info":[{"award-number":["61373034","61170304","2011DFG13000","KZ201210028036"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61373034","61170304","2011DFG13000","KZ201210028036"],"award-info":[{"award-number":["61373034","61170304","2011DFG13000","KZ201210028036"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"International S&T Cooperation Program of China","award":["61373034","61170304","2011DFG13000","KZ201210028036"],"award-info":[{"award-number":["61373034","61170304","2011DFG13000","KZ201210028036"]}]},{"name":"International S&T Cooperation Program of China","award":["61373034","61170304","2011DFG13000","KZ201210028036"],"award-info":[{"award-number":["61373034","61170304","2011DFG13000","KZ201210028036"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Mathematics"],"published-print":{"date-parts":[[2014]]},"abstract":"<jats:p>This paper considers a hybrid I\/O automata model for an automated guided vehicle (AGV) system. A set of key properties of an AGV system are characterized for the correctness of the system. An abstract model is constructed from the hybrid automata model to simplify the proof of the constraints. The two models are equivalent in terms of bisimulation relation. We derive the constraints to ensure the correctness of the properties. We validate the system by analyzing the parameters of the constraints of the AGV system.<\/jats:p>","DOI":"10.1155\/2014\/327465","type":"journal-article","created":{"date-parts":[[2014,5,4]],"date-time":"2014-05-04T17:05:50Z","timestamp":1399223150000},"page":"1-10","source":"Crossref","is-referenced-by-count":0,"title":["A Case Study on Formal Analysis of an Automated Guided Vehicle System"],"prefix":"10.1155","volume":"2014","author":[{"given":"Jie","family":"Zhang","sequence":"first","affiliation":[{"name":"College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, China"},{"name":"University of Tennessee, Knoxville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuntao","family":"Peng","sequence":"additional","affiliation":[{"name":"College of Information Science and Technology, Beijing University of Chemical Technology, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William N. N.","family":"Hung","sequence":"additional","affiliation":[{"name":"Synopsys Inc., Mountain View, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiaojuan","family":"Li","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jindong","family":"Tan","sequence":"additional","affiliation":[{"name":"University of Tennessee, Knoxville, TN, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[{"name":"Beijing Engineering Research Center of High Reliable Embedded System, College of Information Engineering, Capital Normal University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","reference":[{"key":"1","doi-asserted-by":"publisher","DOI":"10.1007\/0-8176-4404-0_5"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1504\/IJMIC.2007.016409"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00067-1"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/5.871300"},{"key":"8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"6","DOI":"10.1007\/3-540-46430-1_5","volume-title":"Modular specification of hybrid systems in charon","volume":"1790","year":"2000"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/5.871311"},{"key":"10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/3-540-45263-X_14","volume-title":"Hybrid models for mobile computing","volume":"1906","year":"2000"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/37.537208"},{"issue":"3","key":"12","first-page":"219","volume":"2","year":"1989","journal-title":"CWI Quarterly"},{"year":"1983","key":"13"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2005.01.036"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1016\/j.ejor.2004.09.020"},{"year":"1989","key":"18"},{"key":"19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Concurrency and automata on infinite sequences","volume":"104","year":"1981"}],"container-title":["Journal of Applied Mathematics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/327465.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/327465.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/jam\/2014\/327465.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,22]],"date-time":"2017-06-22T08:37:40Z","timestamp":1498120660000},"score":1,"resource":{"primary":{"URL":"http:\/\/www.hindawi.com\/journals\/jam\/2014\/327465\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":14,"alternative-id":["327465","327465"],"URL":"https:\/\/doi.org\/10.1155\/2014\/327465","relation":{},"ISSN":["1110-757X","1687-0042"],"issn-type":[{"type":"print","value":"1110-757X"},{"type":"electronic","value":"1687-0042"}],"subject":[],"published":{"date-parts":[[2014]]}}}