{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:00:47Z","timestamp":1762459247219},"reference-count":39,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2015,3,1]],"date-time":"2015-03-01T00:00:00Z","timestamp":1425168000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hybrid logics, which add to the modal description of transition structures the ability to refer to specific states, offer a generic framework to approach the specification and design of reconfigurable systems, i.e., systems with reconfiguration mechanisms governing the dynamic evolution of their execution configurations in response to both external stimuli or internal performance measures. A formal representation of such systems is through transition structures whose states correspond to the different configurations they may adopt. Therefore, each node is endowed with, for example, an algebra, or a first-order structure, to precisely characterise the semantics of the services provided in the corresponding configuration. This paper characterises equivalence and refinement for these sorts of models in a way which is independent of (or parametric on) whatever logic (propositional, equational, fuzzy, etc) is found appropriate to describe the local configurations. A Hennessy\u2013Milner like theorem is proved for hybridised logics.<\/jats:p>","DOI":"10.1007\/s00165-014-0327-6","type":"journal-article","created":{"date-parts":[[2014,12,19]],"date-time":"2014-12-19T07:02:37Z","timestamp":1418972557000},"page":"375-395","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Refinement in hybridised institutions"],"prefix":"10.1145","volume":"27","author":[{"given":"Alexandre","family":"Madeira","sequence":"first","affiliation":[{"name":"HASLab INESC TEC and Univ. Minho, Braga, Portugal"}]},{"given":"Manuel A.","family":"Martins","sequence":"additional","affiliation":[{"name":"CIDMA-Center for R&amp;D in Mathematics and Applications, Department of Mathematics, Univ. Aveiro, Aveiro, Portugal"}]},{"given":"Lu\u00eds S.","family":"Barbosa","sequence":"additional","affiliation":[{"name":"HASLab INESC TEC and Univ. Minho, Braga, Portugal"}]},{"given":"Rolf","family":"Hennicker","sequence":"additional","affiliation":[{"name":"Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen, Munich, Germany"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Agusti-Cullell J Esteva F Garcia P Godo L (1990) Formalizing multiple-valued logics as institutions. In: Bouchon-Meunier B Yager RR Zadeh LA (eds) 3rd International conference on information processing and management of uncertainty in knowledge-based systems (IPMU 90 Paris France July 2\u20136 1990). Lecture notes in computer science vol 521. Springer pp 269\u2013278","DOI":"10.1007\/BFb0028112"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Areces C ten Cate B (2006) Hybrid logics. In: Blackburn P Wolter F van Benthem J (eds) Handbook of modal logics. Elsevier Amsterdam pp 821\u2013868","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"e_1_2_1_2_3_2","unstructured":"Burstall R Diaconescu R (1994) Hiding and behaviour: an institutional approach. In: Roscoe W (ed) A classical mind: essays in honour of C.A.R. Hoare. Prentice-Hall Hertfordshire pp 75\u201392"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Blackburn P de Rijke M Venema Y (2001) Modal logic. Number 53 in Cambridge Tracts in Theoretical Computer Science Cambridge University Press Cambridge","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.09.002"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Beierle C Kern-Isberner G (2005) Looking at probabilistic conditionals from an institutional point of view. In: Kern-Isberner G R\u00f6dder W Kulmann F (eds) Conditionals information and inference (revised selected papers of WCII 2002 Hagen Germany May 13\u201315 2002). Lecture notes in computer science vol 3301. Springer pp 162\u2013179","DOI":"10.1007\/11408017_10"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Brauner T (2010) Hybrid logic and its proof-theory. Applied logic series Springer Netherlands","DOI":"10.1007\/978-94-007-0002-4"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Blackburn P Van Benthem J (2007) Modal logic: a semantic perspective. In: Blackburn P Wolter F van Benthem J (eds) Handbook of modal logic studies in logic and practical reasoning vol 3. Elsevier Amsterdam pp 1\u201382","DOI":"10.1016\/S1570-2464(07)80004-8"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"C\u00eerstea C (2006) An institution of modal logics for coalgebras. J Logic Algebr Progr 67(1\u20132):87\u2013113","DOI":"10.1016\/j.jlap.2005.09.004"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Caleiro C Mateus P Sernadas A Sernadas C (2006) Quantum institutions. In: Futatsugi K Jouannaud J-P Meseguer J (eds) Algebra meaning and computation essays dedicated to Joseph A. Goguen on the occasion of his 65th birthday. Lecture notes in computer science vol 4060. Springer pp 50\u201364","DOI":"10.1007\/11780274_4"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.5555\/1481586"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200910131"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Diaconescu R Madeira A (2014) Encoding hybridized institutions into first order logic. Math Struct Comput Sci. doi:10.1017\/S0960129514000383","DOI":"10.1017\/S0960129514000383"},{"key":"e_1_2_1_2_15_2","unstructured":"Ehrig H Mahr B (1985) Fundamentals of algebraic specification 1: equations and initial semantics. Monographs in theoretical computer science an EATCS Series. Springer Berlin"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/147508.147524"},{"key":"e_1_2_1_2_17_2","unstructured":"Gottwald S (2001) A treatise on many-valued logics. studies in logic and computation vol 9. Research Studies Press Baldock"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-387-77487-9","volume-title":"Universal algebra","author":"Gr\u00e4tzer G","year":"1979"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/262326"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.12775\/LLP.2007.006"},{"key":"e_1_2_1_2_21_2","unstructured":"Madeira A (2013) Foundations and techniques for software reconfigurability. Ph.D. thesis Universidades do Minho Aveiro and Porto (Joint MAP-i Doctoral Programme)"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Madeira A Faria JM Martins MA Barbosa LS (2011) Hybrid specification of reactive systems: an institutional approach. In: Barthe G Pardo A Schneider G (eds) Software engineering and formal methods (SEFM 2011 Montevideo Uruguay November 14\u201318 2011). Lecture notes in computer science vol 7041. Springer pp 269\u2013285","DOI":"10.1007\/978-3-642-24690-6_19"},{"key":"e_1_2_1_2_23_2","unstructured":"Milner R (1989) Communication and concurrency. series in computer science. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Madeira A Martins MA Barbosa LS (2013) Bisimilarity and refinement for hybrid(ised) logics. In: Derrick J Boiten EA Reeves S (eds) Refine-Proceedings 16th international refinement workshop. Electronic proceedings in theoretical computer science vol 115 pp 84\u201398","DOI":"10.4204\/EPTCS.115.6"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Martins MA Madeira A Diaconescu R Barbosa LS (2011) Hybridization of institutions. In: Corradini A KlIn B C\u00eerstea C (eds) Algebra and coalgebra in computer science (CALCO 2011 Winchester UK August 30\u2013September 2 2011). Lecture notes in computer science vol 6859. Springer pp 283\u2013297","DOI":"10.1007\/978-3-642-22944-2_20"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Mossakowski T Maeder C L\u00fcttich K (2007) The heterogeneous tool set Hets. In: Grumberg O Huth M (eds) Tools and algorithms for the construction and analysis of systems (TACAS 2007-Braga Portugal March 24\u2013April 1 2007). Lecture notes in computer science vol 4424. Springer pp 519\u2013522","DOI":"10.1007\/978-3-540-71209-1_40"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Madeira A Neves R Martins MA Barbosa LS (2013) When even the interface evolves. In: Wang H Banach R (eds) Proceedings of TASE (7th IEEE symposium on theoretical aspects of software engineering Birmingham July 2013). IEEE Computer Society pp 79\u201382","DOI":"10.1109\/TASE.2013.19"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Mossakowski T Roggenbach M (2006) Structured CSP\u2014a process algebra as an institution. In: Fiadeiro JL Schobbens P-Y (eds) Recent trends in algebraic development techniques (revised selected papers of WADT 2006 La Roche en Ardenne Belgium June 1\u20133 2006). Lecture notes in computer science vol 4409. Springer pp 92\u2013110","DOI":"10.1007\/978-3-540-71998-4_6"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Neves R Madeira A Martins MA Barbosa LS (2013) Hybridisation at work. In: Heckel R Milius S (eds) Algebra and coalgebra in computer science\u20145th international conference CALCO 2013 Warsaw Poland September 3\u20136 2013. Proceedings Lecture notes in computer science vol 8089 Springer pp 340\u2013345","DOI":"10.1007\/978-3-642-40206-7_28"},{"key":"#cr-split#-e_1_2_1_2_30_2.1","unstructured":"Park D (1981) Concurrency and automata on infinite sequences. In: Deussen P"},{"key":"#cr-split#-e_1_2_1_2_30_2.2","unstructured":"(ed) Theoretical computer science (5th GI-conference Karlsruhe Germany March 23-25 1981). Lecture notes in computer science vol 104. Springer pp 167-183"},{"key":"#cr-split#-e_1_2_1_2_31_2.1","doi-asserted-by":"crossref","unstructured":"Sannella D (1999) Algebraic specification and program development by stepwise refinement. In: Bossi A","DOI":"10.1007\/978-3-642-59851-7_8"},{"key":"#cr-split#-e_1_2_1_2_31_2.2","unstructured":"(ed) Logic-based program synthesis and transformation. Lecture notes in computer science vol 1817. Springer Venezia Italy pp 1-9"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Sangiorgi D (2009) On the origins of bisimulation and coinduction. ACM Trans Progr Lang Syst 31(4):1\u201341. doi:10.1145\/1516507.1516510","DOI":"10.1145\/1516507.1516510"},{"key":"e_1_2_1_2_33_2","first-page":"74","article-title":"An overview on software reconfiguration","volume":"1","author":"Szepesia R","year":"2011","journal-title":"Theory Appl Math Comput Sci"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.11.020"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sannella D Tarlecki A (2012) Foundations of algebraic specification and formal software development. Monographs on theoretical computer science an EATCS series. Springer","DOI":"10.1007\/978-3-642-17336-3"},{"key":"e_1_2_1_2_36_2","unstructured":"Tarlecki A (2003) Abstract specification theory: an overview. In: Broy M Pizka M (eds) Models algebras and logics of engineering software. NATO science series computer and systems sciences vol 191. IOS Press pp 43\u201379"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"ten Cate BD (2005) Model theory for extended modal languages. Ph.D. thesis Institute for Logic Language and Computation Universiteit van Amsterdam","DOI":"10.2178\/jsl\/1107298517"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0327-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0327-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0327-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,30]],"date-time":"2023-07-30T19:50:25Z","timestamp":1690746625000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0327-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,3]]}},"alternative-id":["10.1007\/s00165-014-0327-6"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0327-6","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3]]}}}