{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:14:52Z","timestamp":1771485292034,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>Hybrid systems are manifest in both the natural and the engineered world, and their complex nature, mixing discrete control and continuous evolution, make it difficult to predict their behaviour. In recent years several process algebras for modelling hybrid systems have appeared in the literature, aimed at addressing this problem. These all assume that continuous variables in the system are modelled monolithically, often with differential equations embedded explicitly in the syntax of the process algebra expression. In HYPE an alternative approach is taken which offers finer-grained modelling with each flow or influence affecting a variable modelled separately. The overall behaviour then emerges as the composition of flows. In this paper we give a detailed account of the HYPE process algebra, its semantics, and its use for verification of systems. We establish both syntactic conditions (well-definedness) and operational restrictions (well-behavedness) to ensure reasonable behaviour in HYPE models. Furthermore we consider how the equivalence relation defined for HYPE relates to other relations previously proposed in the literature, demonstrating that our fine-grained approach leads to a more discriminating notion of equivalence. We present the HYPE model of a standard hybrid system example, both establishing that our approach can reproduce the previously obtained results and demonstrating how our compositional approach supports variations of the problem in a straightforward and flexible way.<\/jats:p>","DOI":"10.1007\/s00165-011-0189-0","type":"journal-article","created":{"date-parts":[[2011,8,12]],"date-time":"2011-08-12T10:44:26Z","timestamp":1313145866000},"page":"503-541","source":"Crossref","is-referenced-by-count":13,"title":["HYPE: Hybrid modelling by composition of flows"],"prefix":"10.1145","volume":"25","author":[{"given":"Vashti","family":"Galpin","sequence":"first","affiliation":[{"name":"Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Informatics Forum, 10 Crichton Street, EH8 9AB, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Bortolussi","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, University of Trieste, Trieste, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jane","family":"Hillston","sequence":"additional","affiliation":[{"name":"Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Informatics Forum, 10 Crichton Street, EH8 9AB, Edinburgh, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.10.004"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Akman OE Guerriero ML Loewe L Troein C (2010) Complementary approaches to understanding the plant circadian clock. In: Proceedings of FBTC\u201910 EPTCS vol 19 pp 1\u201319","DOI":"10.4204\/EPTCS.19.1"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"#cr-split#-e_1_2_1_2_4_2.1","doi-asserted-by":"crossref","unstructured":"Antoniotti M Mishra B Piazza C Policriti A Simeoni M (2003) Modeling cellular behavior with hybrid automata: bisimulation and collapsing. In: Priami C","DOI":"10.1007\/3-540-36481-1_6"},{"key":"#cr-split#-e_1_2_1_2_4_2.2","unstructured":"(ed) Proceedings of CMSB 2003. LNCS vol 2602 pp 57-74"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bortolussi L Galpin V Hillston J (2010) HYPE with stochastic events. In: Proceedings of QAPL 2011 EPTCS vol 57 pp 120\u2013133","DOI":"10.4204\/EPTCS.57.9"},{"key":"e_1_2_1_2_6_2","unstructured":"Bortolussi L Galpin V Hillston J (2010) Modeling hybrid systems with stochastic events in HYPE. In: Proceedings of the 9th workshop on process algebra and stochastically timed activities (PASTA) pp 24\u201328"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.04.019"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Bortolusssi L Policriti A (2008) Hybrid approximation of stochastic process algebras for systems biology. In: IFAC World Congress Seoul South Korea July 2008","DOI":"10.3182\/20080706-5-KR-1001.02132"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Bortolussi L Policriti A (2009) Hybrid semantics of stochastic programs with dynamic reconfiguration. In: Proceedings of COMPMOD 2009 EPTCS vol 6 pp 63\u201376","DOI":"10.4204\/EPTCS.6.5"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1177\/0037549708097215"},{"key":"e_1_2_1_2_11_2","unstructured":"Cuijpers PJL Reniers MA (2003) Hybrid process algebra. Computer Science Reports CSR 03-07 Department of Computer Science Eindhoven Technical University"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.02.001"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Davis MHA (1993) Markov models and optimization. Chapman & Hall","DOI":"10.1007\/978-1-4899-4483-2"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Deshpande A G\u00f6ll\u00fc A Varaiya P (1996) SHIFT: a formalism and a programming language for dynamic networks of hybrid automata. In: Antsaklis PJ Kohn W Nerode A Sastry S (eds) Proceedings of hybrid systems IV. LNCS vol 1273 pp 113\u2013133","DOI":"10.1007\/BFb0031558"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00361-X"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Davoren JM Tabuada P (2007) On simulations and bisimulations of general flow systems. In: Bemporad A Bicchi A Buttazzo GC (eds) Proceedings of HSCC 2007. LNCS vol 4416 pp 145\u2013158","DOI":"10.1007\/978-3-540-71493-4_14"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1038\/35002125"},{"key":"e_1_2_1_2_18_2","unstructured":"Galpin V (2010) Modelling a circadian clock with HYPE. In: Proceedings of the 9th workshop on process algebra and stochastically timed activities (PASTA) pp 92\u201398"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Galpin V Bortolussi L Hillston J (2009) Hype: a process algebra for compositional flows and emergent behaviour. In: Bravetti M Zavattaro G (eds) Proceedings of CONCUR 2009. LNCS vol 5710. Springer Berlin pp 305\u2013320","DOI":"10.1007\/978-3-642-04081-8_21"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.004"},{"key":"e_1_2_1_2_21_2","unstructured":"Galpin V Hillston J Bortolussi L (2010) A stochastic hybrid process algebra (poster). In: Models and logics for quantitative analysis (MLQA 2010) Edinburgh July 2010"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016001318739"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: LICS pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_2_1_2_24_2","first-page":"265","volume-title":"Hybrid systems. LNCS, vol 999","author":"Henzinger TA","year":"1994"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hillston J (2005) Fluid flow approximation of PEPA models. In: Second international conference on the quantitative evaluation of systems (QEST 2005). IEEE Computer Society pp 33\u201343","DOI":"10.1109\/QEST.2005.12"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA Kopke PW Puri A and Varaiya P (1995) What\u2019s decidable about hybrid automata? In: Proceedings of the twenty-seventh annual ACM symposium on theory of computing STOC \u201995 pp 373\u2013382","DOI":"10.1145\/225058.225162"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.045"},{"key":"e_1_2_1_2_28_2","unstructured":"Khadim U (2006) A comparative study of process algebras for hybrid systems. Computer Science Report CSR 06-23 Technische Universiteit Eindhoven. http:\/\/alexandria.tue.nl\/extra1\/wskrap\/publichtml\/200623.pdf"},{"key":"e_1_2_1_2_29_2","unstructured":"Khadim U (2008) Process algebras for hybrid systems: comparison and development. PhD thesis IPA Technische Universiteit Eindhoven"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/PL00009858"},{"key":"e_1_2_1_2_31_2","unstructured":"Milner R (1989) Communication and concurrency. Prentice Hall"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.03.002"},{"key":"e_1_2_1_2_33_2","unstructured":"Paynter HM (1961) Analysis and design of engineering systems. MIT Press"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00547-9"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Rounds WC Song H (2003) The \u03c6 -calculus: a language for distributed control of reconfigurable embedded systems. In: Maler O Pnueli A (eds) Proceedings of HSCC 2003. LNCS vol 2623 pp 435\u2013449","DOI":"10.1007\/3-540-36580-X_32"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008387132533"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Tribastone M Gilmore S Hillston J (2010) Scalable differential analysis of process algebra models. IEEE Trans Softw Eng. doi:10.1109\/TSE.201082","DOI":"10.1109\/QEST.2010.45"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.10.005"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"van Glabbeek RJ (1990) The linear time-branching time spectrum (extended abstract). In: Proceedings of CONCUR 90. LNCS vol 458. Springer Berlin pp 278\u2013297","DOI":"10.1007\/BFb0039066"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0189-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0189-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0189-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:56Z","timestamp":1641484556000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0189-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":40,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1007\/s00165-011-0189-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0189-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}