{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:19:26Z","timestamp":1759033166176},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2013,12,5]],"date-time":"2013-12-05T00:00:00Z","timestamp":1386201600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,6]]},"DOI":"10.1007\/s10703-013-0201-9","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T13:49:27Z","timestamp":1386164967000},"page":"240-263","source":"Crossref","is-referenced-by-count":6,"title":["A modal characterization of alternating approximate bisimilarity"],"prefix":"10.1007","volume":"44","author":[{"given":"Jinjin","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Zhu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,12,5]]},"reference":[{"key":"201_CR1","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1007\/BFb0018361","volume-title":"Proceedings of the category theory and computer science","author":"P Aczel","year":"1989","unstructured":"Aczel P, Mendler N (1989) A final coalgebra theorem. In: Proceedings of the category theory and computer science. Springer, Berlin, pp\u00a0357\u2013365"},{"key":"201_CR2","first-page":"165","volume-title":"Proceedings of the international conference on concurrency theory (CONCUR)","author":"R Alur","year":"1998","unstructured":"Alur R, Henzinger T, Kupferman O, Vardi M (1998) Alternating refinement relations. In: Proceedings of the international conference on concurrency theory (CONCUR). Springer, Berlin, pp\u00a0165\u2013178"},{"issue":"7","key":"201_CR3","doi-asserted-by":"crossref","first-page":"971","DOI":"10.1109\/5.871304","volume":"88","author":"R Alur","year":"2000","unstructured":"Alur R, Henzinger T, Lafferriere G, Pappas G (2000) Discrete abstractions of hybrid systems. Proc IEEE 88(7):971\u2013984","journal-title":"Proc IEEE"},{"issue":"5","key":"201_CR4","doi-asserted-by":"crossref","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur R, Henzinger T, Kupferman O (2002) Alternating-time temporal logic. J ACM 49(5):672\u2013713","journal-title":"J ACM"},{"issue":"10","key":"201_CR5","doi-asserted-by":"crossref","first-page":"1422","DOI":"10.1080\/00207179.2012.686672","volume":"85","author":"APG Borri","year":"2012","unstructured":"Borri APG, Di Benedetto M (2012) Symbolic models for nonlinear control systems affected by disturbances. Int J Control 85(10):1422\u20131432","journal-title":"Int J Control"},{"key":"201_CR6","first-page":"141","volume-title":"Proceedings of the international conference on concurrency theory (CONCUR)","author":"F Breugel van","year":"2005","unstructured":"Breugel F\u00a0van (2005) A behavioural pseudometric for metric labelled transition systems. In: Proceedings of the international conference on concurrency theory (CONCUR). Springer, Berlin, pp\u00a0141\u2013155"},{"issue":"1","key":"201_CR7","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.tcs.2004.09.035","volume":"331","author":"F Breugel van","year":"2005","unstructured":"Breugel F\u00a0van, Worrell J (2005) A behavioural pseudometric for probabilistic transition systems. Theor Comput Sci 331(1):115\u2013142","journal-title":"Theor Comput Sci"},{"key":"201_CR8","first-page":"1","volume":"4(2:2)","author":"F Breugel van","year":"2008","unstructured":"Breugel F\u00a0van, Sharma B, Worrell J (2008) Approximating a behavioural pseudometric without discount for probabilistic systems. Log Methods Comput Sci 4(2:2):1\u201323","journal-title":"Log Methods Comput Sci"},{"key":"201_CR9","first-page":"191","volume-title":"Proceedings of the 14th international conference on hybrid systems: computation and control","author":"J C\u00e1mara","year":"2011","unstructured":"C\u00e1mara J, Girard A, G\u00f6ssler G (2011) Synthesis of switching controllers using approximately bisimilar multiscale abstractions. In: Proceedings of the 14th international conference on hybrid systems: computation and control. ACM, New York, pp\u00a0191\u2013200"},{"issue":"2","key":"201_CR10","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1109\/TSE.2008.106","volume":"35","author":"L Alfaro De","year":"2009","unstructured":"De Alfaro L, Faella M, Stoelinga M (2009) Linear and branching system metrics. IEEE Trans Softw Eng 35(2):258\u2013273","journal-title":"IEEE Trans Softw Eng"},{"key":"201_CR11","unstructured":"Desharnais J (1999) Labelled Markov processes. Ph.D. thesis, McGill University"},{"issue":"3","key":"201_CR12","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/j.tcs.2003.09.013","volume":"318","author":"J Desharnais","year":"2004","unstructured":"Desharnais J, Gupta V, Jagadeesan R, Panangaden P (2004) Metrics for labelled Markov processes. Theor Comput Sci 318(3):323\u2013354","journal-title":"Theor Comput Sci"},{"key":"201_CR13","first-page":"443","volume-title":"Proceedings of the IFIPWG 2.2\/2.3 working conf. on programming concepts and methods","author":"A Giacalone","year":"1990","unstructured":"Giacalone A, Jou CSS (1990) Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the IFIPWG 2.2\/2.3 working conf. on programming concepts and methods, Sea of Gallilee. North-Holland, Amsterdam, pp 443\u2013458"},{"key":"201_CR14","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid systems: computation and control","author":"A Girard","year":"2005","unstructured":"Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Hybrid systems: computation and control. Springer, Berlin, pp\u00a0291\u2013305"},{"key":"201_CR15","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/978-3-540-71493-4_20","volume-title":"Proceedings of the hybrid systems: computation and control","author":"A Girard","year":"2007","unstructured":"Girard A (2007) Approximately bisimilar finite abstractions of stable linear systems. In: Proceedings of the hybrid systems: computation and control. IEEE Press, New York, pp\u00a0231\u2013244"},{"key":"201_CR16","unstructured":"Girard A, Metrics for approximate transition systems simulation and equivalence (MATSSE). http:\/\/ljk.imag.fr\/membres\/Antoine.Girard\/Software\/Matisse\/index.html"},{"issue":"5","key":"201_CR17","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TAC.2007.895849","volume":"52","author":"A Girard","year":"2007","unstructured":"Girard A, Pappas G (2007) Approximation metrics for discrete and continuous systems. IEEE Trans Autom Control 52(5):782\u2013798","journal-title":"IEEE Trans Autom Control"},{"issue":"2","key":"201_CR18","doi-asserted-by":"crossref","first-page":"566","DOI":"10.1016\/j.automatica.2008.09.016","volume":"45","author":"A Girard","year":"2009","unstructured":"Girard A, Pappas G (2009) Hierarchical control system design using approximate simulation. Automatica 45(2):566\u2013571","journal-title":"Automatica"},{"issue":"5","key":"201_CR19","doi-asserted-by":"crossref","first-page":"568","DOI":"10.3166\/ejc.17.568-578","volume":"17","author":"A Girard","year":"2011","unstructured":"Girard A, Pappas G (2011) Approximate bisimulation: a bridge between computer science and control theory. Eur J Control 17(5):568\u2013578","journal-title":"Eur J Control"},{"issue":"1","key":"201_CR20","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M Hennessy","year":"1985","unstructured":"Hennessy M, Milner R (1985) Algebraic laws for nondeterminism and concurrency. J ACM 32(1):137\u2013161","journal-title":"J ACM"},{"key":"201_CR21","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/978-3-540-78929-1_21","volume-title":"Proceedings of the hybrid systems: computation and control","author":"M Kloetzer","year":"2008","unstructured":"Kloetzer M, Belta C (2008) Dealing with nondeterminism in symbolic control. In: Proceedings of the hybrid systems: computation and control. Springer, Berlin, pp\u00a0287\u2013300"},{"key":"201_CR22","volume-title":"Theorie der endlichen und unendlichen Graphen: Kombinatorische Topologie der Strekenkomplexe","author":"D K\u00f6nig","year":"1936","unstructured":"K\u00f6nig D (1936) Theorie der endlichen und unendlichen Graphen: Kombinatorische Topologie der Strekenkomplexe"},{"key":"201_CR23","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/3-540-58027-1_8","volume-title":"Proceeding of the mathematical foundations of programming semantics","author":"K Larsen","year":"1994","unstructured":"Larsen K, Yi W (1994) Time abstracted bisimulation: implicit specifications and decidability. In: Proceeding of the mathematical foundations of programming semantics. Springer, Berlin, pp\u00a0160\u2013176"},{"key":"201_CR24","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Proceedings of the 5th GI-conference on theoretical computer science","author":"D Park","year":"1981","unstructured":"Park D (1981) Concurrency and automata on infinite sequences. In: Proceedings of the 5th GI-conference on theoretical computer science. Springer, Berlin, pp\u00a0167\u2013183"},{"key":"201_CR25","first-page":"251","volume-title":"Proceedings of the 47th IEEE conference on decision and control","author":"G Pola","year":"2008","unstructured":"Pola G, Tabuada P (2008) Symbolic models for nonlinear control systems affected by disturbances. In: Proceedings of the 47th IEEE conference on decision and control. IEEE Press, New York, pp\u00a0251\u2013256"},{"key":"201_CR26","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1137\/070698580","volume":"48","author":"G Pola","year":"2009","unstructured":"Pola G, Tabuada P (2009) Symbolic models for nonlinear control systems: alternating approximate bisimulations. SIAM J Control Optim 48:719\u2013733","journal-title":"SIAM J Control Optim"},{"issue":"10","key":"201_CR27","doi-asserted-by":"crossref","first-page":"2508","DOI":"10.1016\/j.automatica.2008.02.021","volume":"44","author":"G Pola","year":"2008","unstructured":"Pola G, Girard A, Tabuada P (2008) Approximately bisimilar symbolic models for nonlinear control systems. Automatica 44(10):2508\u20132516","journal-title":"Automatica"},{"issue":"6","key":"201_CR28","doi-asserted-by":"crossref","first-page":"1406","DOI":"10.1109\/TAC.2008.925824","volume":"53","author":"P Tabuada","year":"2008","unstructured":"Tabuada P (2008) An approximate simulation approach to symbolic control. IEEE Trans Autom Control 53(6):1406\u20131418","journal-title":"IEEE Trans Autom Control"},{"key":"201_CR29","first-page":"634","volume-title":"Proceedings of the 42nd IEEE conference on decision and control, 2003","author":"P Tabuada","year":"2003","unstructured":"Tabuada P, Pappas G (2003) Finite bisimulations of controllable linear systems. In: Proceedings of the 42nd IEEE conference on decision and control, 2003, vol\u00a01. IEEE Press, New York, pp\u00a0634\u2013639"},{"key":"201_CR30","first-page":"3366","volume-title":"Proceedings of the 42nd IEEE conference on decision and control, 2003","author":"P Tabuada","year":"2003","unstructured":"Tabuada P, Pappas G (2003) From discrete specifications to hybrid control. In: Proceedings of the 42nd IEEE conference on decision and control, 2003, vol\u00a04. IEEE Press, New York, pp\u00a03366\u20133371"},{"issue":"12","key":"201_CR31","doi-asserted-by":"crossref","first-page":"1862","DOI":"10.1109\/TAC.2006.886494","volume":"51","author":"P Tabuada","year":"2006","unstructured":"Tabuada P, Pappas G (2006) Linear time logic control of discrete-time linear systems. IEEE Trans Autom Control 51(12):1862\u20131877","journal-title":"IEEE Trans Autom Control"},{"key":"201_CR32","first-page":"502","volume-title":"Proceedings of the international conference on concurrency theory (CONCUR)","author":"Y Wang","year":"1990","unstructured":"Wang Y (1990) Real-time behaviour of asynchronous agents. In: Proceedings of the international conference on concurrency theory (CONCUR). Springer, Berlin, pp\u00a0502\u2013520"},{"issue":"1\u20132","key":"201_CR33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/S0304-3975(01)00124-4","volume":"275","author":"M Ying","year":"2002","unstructured":"Ying M (2002) Bisimulation indexes and their applications. Theor Comput Sci 275(1\u20132):1\u201368","journal-title":"Theor Comput Sci"},{"issue":"9","key":"201_CR34","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/s00236-005-0168-0","volume":"41","author":"M Ying","year":"2005","unstructured":"Ying M (2005) \u03c0-Calculus with noisy channels. Acta Inform 41(9):525\u2013593","journal-title":"Acta Inform"},{"issue":"3","key":"201_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1507244.1507249","volume":"10","author":"M Ying","year":"2009","unstructured":"Ying M, Feng Y, Duan R, Ji Z (2009) An algebra of quantum processes. ACM Trans Comput Log 10(3):1\u201336","journal-title":"ACM Trans Comput Log"},{"issue":"1","key":"201_CR36","first-page":"85","volume":"1","author":"J Zhang","year":"2007","unstructured":"Zhang J, Zhu Z (2007) A modal characterization of \u03bb-bisimilarity. Int J Softw Inform 1(1):85\u201399","journal-title":"Int J Softw Inform"},{"issue":"3","key":"201_CR37","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/j.entcs.2008.11.022","volume":"220","author":"J Zhang","year":"2008","unstructured":"Zhang J, Zhu Z (2008) A behavioural pseudometric based on \u03bb-bisimilarity. Electron Notes Theor Comput Sci 220(3):115\u2013127","journal-title":"Electron Notes Theor Comput Sci"},{"issue":"8","key":"201_CR38","doi-asserted-by":"crossref","first-page":"953","DOI":"10.1016\/j.ic.2008.06.001","volume":"206","author":"J Zhang","year":"2008","unstructured":"Zhang J, Zhu Z (2008) Characterize branching distance in terms of (\u03b7,\u03b1)-bisimilarity. Inf Comput 206(8):953\u2013965","journal-title":"Inf Comput"},{"key":"201_CR39","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.tcs.2012.03.026","volume":"446","author":"C Zhou","year":"2012","unstructured":"Zhou C, Ying M (2012) Approximating Markov processes through filtration. Theor Comput Sci 446:75\u201397","journal-title":"Theor Comput Sci"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0201-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-013-0201-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-013-0201-9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T18:05:54Z","timestamp":1559239554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-013-0201-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,5]]},"references-count":39,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2014,6]]}},"alternative-id":["201"],"URL":"https:\/\/doi.org\/10.1007\/s10703-013-0201-9","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,5]]}}}