{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,10,22]],"date-time":"2022-10-22T09:26:52Z","timestamp":1666430812255},"reference-count":45,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[2008,9,1]],"date-time":"2008-09-01T00:00:00Z","timestamp":1220227200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,8,22]],"date-time":"2013-08-22T00:00:00Z","timestamp":1377129600000},"content-version":"vor","delay-in-days":1816,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2008,9]]},"DOI":"10.1016\/j.tcs.2008.03.010","type":"journal-article","created":{"date-parts":[[2008,3,27]],"date-time":"2008-03-27T20:24:05Z","timestamp":1206649445000},"page":"186-201","source":"Crossref","is-referenced-by-count":6,"title":["On model checking multiple hybrid views"],"prefix":"10.1016","volume":"404","author":[{"given":"Altaf","family":"Hussain","sequence":"first","affiliation":[]},{"given":"Michael","family":"Huth","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2008.03.010_b1","unstructured":"A. Antonik, January 2007, M.Phil.\/Ph.D. Transfer Report, Department of Computing, Imperial College London, United Kingdom"},{"key":"10.1016\/j.tcs.2008.03.010_b2","series-title":"Proceedings of the 13th Conference on Computer Aided Verification","first-page":"260","article-title":"The SLAM Toolkit","volume":"vol. 2102","author":"Ball","year":"2001"},{"key":"10.1016\/j.tcs.2008.03.010_b3","series-title":"Proceedings of Middleware\u201904, ACM\/IFIP\/USENIX International Middleware Conference","first-page":"493","article-title":"Platform independent model transformation based on triple","volume":"vol. 3231","author":"Billig","year":"2004"},{"key":"10.1016\/j.tcs.2008.03.010_b4","series-title":"Proceedings of the 11th Conference on Computer Aided Verification","first-page":"274","article-title":"Model checking partial state spaces with 3-valued temporal logics","volume":"vol. 1633","author":"Bruns","year":"1999"},{"key":"10.1016\/j.tcs.2008.03.010_b5","series-title":"Proceedings of the 11th International Conference on Concurrency Theory","first-page":"168","article-title":"Generalized model checking: Reasoning about partial state spaces","volume":"vol. 1877","author":"Bruns","year":"2000"},{"issue":"4","key":"10.1016\/j.tcs.2008.03.010_b6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/990010.990011","article-title":"Multi-valued symbolic model-checking","volume":"12","author":"Chechik","year":"2003","journal-title":"ACM Transactions on Software Engineering and Methodology"},{"key":"10.1016\/j.tcs.2008.03.010_b7","series-title":"Logic of Programs Workshop","article-title":"Synthesis of synchronization skeletons for branching time temporal logic","volume":"vol. 131","author":"Clarke","year":"1981"},{"issue":"1\u20133","key":"10.1016\/j.tcs.2008.03.010_b8","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0167-6423(99)00045-3","article-title":"Combinations of abstract domains for logic programming: open product and generic pattern construction","volume":"38","author":"Cortesi","year":"2000","journal-title":"Science of Computer Programming"},{"key":"10.1016\/j.tcs.2008.03.010_b9","series-title":"Proceedings of the 4th ACM Symp. on Principles of Programming Languages","first-page":"238","article-title":"Abstract interpretation: A unified lattice model for static analysis of programs","author":"Cousot","year":"1977"},{"key":"10.1016\/j.tcs.2008.03.010_b10","series-title":"Conference Record of the Sixth Annual Symposium on Principles of Programming Languages","first-page":"269","article-title":"Systematic design of program analysis frameworks","author":"Cousot","year":"1979"},{"key":"10.1016\/j.tcs.2008.03.010_b11","series-title":"Conference Record of the 27th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","first-page":"12","article-title":"Temporal abstract interpretation","author":"Cousot","year":"2000"},{"key":"10.1016\/j.tcs.2008.03.010_b12","unstructured":"D. Dams, 1996, Abstract interpretation and partition refinement for model checking, Ph.D. Thesis, Technische Universiteit Eindhoven, The Netherlands"},{"issue":"2","key":"10.1016\/j.tcs.2008.03.010_b13","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1145\/244795.244800","article-title":"Abstract interpretation of reactive systems","volume":"19","author":"Dams","year":"1997","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10.1016\/j.tcs.2008.03.010_b14","series-title":"Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science","first-page":"335","article-title":"The existence of finite abstractions for branching time model checking","author":"Dams","year":"2004"},{"key":"10.1016\/j.tcs.2008.03.010_b15","series-title":"Proceedings of 6th International Conference on Verification, Model Checking and Abstract Interpretation","first-page":"216","article-title":"Automata as Abstractions","volume":"vol. 3385","author":"Dams","year":"2004"},{"issue":"2","key":"10.1016\/j.tcs.2008.03.010_b16","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1016\/j.entcs.2004.11.031","article-title":"Characteristic \u03bc-calculus formula for an underspecified transition system","volume":"128","author":"Fecher","year":"2005","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"10.1016\/j.tcs.2008.03.010_b17","doi-asserted-by":"crossref","first-page":"55","DOI":"10.3233\/FI-1992-171-205","article-title":"Many-valued modal logics II","volume":"17","author":"Fitting","year":"1992","journal-title":"Fundamenta Informaticae"},{"issue":"3","key":"10.1016\/j.tcs.2008.03.010_b18","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.jal.2005.06.010","article-title":"Model checking hybrid logics (with an application to semistructured data)","volume":"4","author":"Franceschet","year":"2005","journal-title":"Journal of Applied Logic"},{"issue":"2","key":"10.1016\/j.tcs.2008.03.010_b19","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/s00165-005-0059-8","article-title":"Model checking, testing, and verification working together","volume":"17","author":"Gunter","year":"2005","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.tcs.2008.03.010_b20","series-title":"Proceedings of the 14th International Conference on Computer Aided Verification","first-page":"137","article-title":"Automatic abstraction using generalized model checking","volume":"vol. 2404","author":"Godefroid","year":"2002"},{"key":"10.1016\/j.tcs.2008.03.010_b21","series-title":"Proceedings of 4th Conference on Verification, Model Checking and Abstract Interpretation","first-page":"206","article-title":"On the expressiveness of 3-valued models","volume":"vol. 2575","author":"Godefroid","year":"2003"},{"issue":"1","key":"10.1016\/j.tcs.2008.03.010_b22","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1145\/147508.147524","article-title":"Institutions: Abstract model theory for specification and programming","volume":"39","author":"Goguen","year":"1992","journal-title":"Journal of the ACM"},{"key":"10.1016\/j.tcs.2008.03.010_b23","series-title":"Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology","first-page":"26","article-title":"Distance Functions for Defaults in Reactive Systems","volume":"vol. 1816","author":"Guerra","year":"2000"},{"key":"10.1016\/j.tcs.2008.03.010_b24","doi-asserted-by":"crossref","unstructured":"T. Henzinger, R. Jhala, R. Majumdar, G. Sutre, Lazy abstraction, in: Proceedings of the 29th ACM Symposium on Principles of Programming Languages, Portland, January 2002, pp. 58\u201370","DOI":"10.1145\/503272.503279"},{"key":"10.1016\/j.tcs.2008.03.010_b25","unstructured":"A. Hussain, M. Huth, On model checking multiple hybrid views, in: Preliminary Proceedings of the First International Symposium on Leveraging Applications of Formal Method. Paphos, Cyprus, Technical Report TR-2004-6, Department of Computer Science, University of Cyprus, 30 October\u20132 November 2004, pp. 235\u2013242"},{"key":"10.1016\/j.tcs.2008.03.010_b26","series-title":"The Proceedings of the 21th Annual Conference on Mathematical Foundations of Programming Semantics","first-page":"401","article-title":"Automata games for multiple-model checking","author":"Hussain","year":"2006"},{"key":"10.1016\/j.tcs.2008.03.010_b27","series-title":"Proceedings of the Second Workshop in Quantitative Aspects of Programming Languages, March 2004","first-page":"61","article-title":"Abstraction and probabilities for hybrid logics","volume":"vol. 112","author":"Huth","year":"2005"},{"issue":"1","key":"10.1016\/j.tcs.2008.03.010_b28","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-1(1:1)2005","article-title":"Labelled transition systems as a stone space","volume":"1","author":"Huth","year":"2005","journal-title":"Logical Methods in Computer Science"},{"issue":"2","key":"10.1016\/j.tcs.2008.03.010_b29","doi-asserted-by":"crossref","first-page":"113","DOI":"10.1007\/s00165-005-0063-z","article-title":"Refinement is complete for implementations","volume":"17","author":"Huth","year":"2005","journal-title":"Formal Aspects of Computing"},{"key":"10.1016\/j.tcs.2008.03.010_b30","series-title":"Proceedings of the European Symposium on Programming","first-page":"155","article-title":"Modal transition systems: a foundation for three-valued program analysis","author":"Huth","year":"2001"},{"issue":"4","key":"10.1016\/j.tcs.2008.03.010_b31","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129504004268","article-title":"A domain equation for refinement of partial systems","volume":"14","author":"Huth","year":"2004","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/j.tcs.2008.03.010_b32","series-title":"Automatic Verification Methods for Finite State Systems","first-page":"232","article-title":"Modal specifications","volume":"vol. 407","author":"Larsen","year":"1989"},{"key":"10.1016\/j.tcs.2008.03.010_b33","series-title":"Proc. of the Fifth Annual IEEE Symposium on Logic in Computer Science","first-page":"108","article-title":"Equation solving using modal transition systems","author":"Larsen","year":"1990"},{"key":"10.1016\/j.tcs.2008.03.010_b34","series-title":"Tools and Algorithms for Construction and Analysis of Systems, 1st International Workshop","first-page":"17","article-title":"A constraint oriented proof methodology based on modal transition systems","volume":"vol. 1019","author":"Larsen","year":"1995"},{"key":"10.1016\/j.tcs.2008.03.010_b35","series-title":"Proceedings of the 3rd Annual Symposium on Logic in Computer Science","first-page":"203","article-title":"A modal process logic","author":"Larsen","year":"1988"},{"key":"10.1016\/j.tcs.2008.03.010_b36","series-title":"Reasoning and Revision in Hybrid Representation Systems","volume":"vol. 422","author":"Nebel","year":"1990"},{"key":"10.1016\/j.tcs.2008.03.010_b37","unstructured":"C. Nentwich, March 2005. Managing the Consistency of Distributed Documents. Ph.D. Thesis, University College London, University of London, London, United Kingdom"},{"issue":"2","key":"10.1016\/j.tcs.2008.03.010_b38","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/514183.514186","article-title":"xlinkit: a consistency checking and smart link generation service","volume":"2","author":"Nentwich","year":"2002","journal-title":"ACM Transactions on Internet Technology"},{"issue":"10","key":"10.1016\/j.tcs.2008.03.010_b39","doi-asserted-by":"crossref","first-page":"760","DOI":"10.1109\/32.328995","article-title":"A framework for expressing the relationships between multiple views in requirements specification","volume":"20","author":"Nuseibeh","year":"1994","journal-title":"IEEE Transactions on Software Engineering"},{"key":"10.1016\/j.tcs.2008.03.010_b40","doi-asserted-by":"crossref","unstructured":"A. Pnueli, 1977. The temporal logic of programs, in: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science, pp. 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"10.1016\/j.tcs.2008.03.010_b41","unstructured":"J.P. Quielle, J. Sifakis, Specification and verification of concurrent systems in CAESAR, in: Proceedings of the 5th International Symposium on Programming, 1981"},{"key":"10.1016\/j.tcs.2008.03.010_b42","series-title":"Proceedings of the 30th Hawaii International Conference on System Sciences","first-page":"44","article-title":"A three-layer model for schema management","volume":"vol. 1","author":"Roantree","year":"1997"},{"key":"10.1016\/j.tcs.2008.03.010_b43","doi-asserted-by":"crossref","unstructured":"M. Sagiv, T. Reps, R. Wilhelm, January 20-22, San Antonio, Texas 1999. Parametric Shape Analysis via 3-Valued Logic, in: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 105\u2013118","DOI":"10.1145\/292540.292552"},{"key":"10.1016\/j.tcs.2008.03.010_b44","series-title":"Proceedings of the 1st International Joint Conference on Automated Reasoning","first-page":"76","article-title":"The Hybrid \u03bc-calculus","volume":"vol. 2083","author":"Sattler","year":"2001"},{"issue":"6","key":"10.1016\/j.tcs.2008.03.010_b45","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1041685.1029904","article-title":"Merging partial behavioural models","volume":"29","author":"Uchitel","year":"2004","journal-title":"ACM SIGSOFT Notes"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397508002181?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397508002181?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2021,9,6]],"date-time":"2021-09-06T17:23:52Z","timestamp":1630949032000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397508002181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9]]},"references-count":45,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,9]]}},"alternative-id":["S0304397508002181"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2008.03.010","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2008,9]]}}}