{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:17Z","timestamp":1760202737948,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2017,7,1]],"date-time":"2017-07-01T00:00:00Z","timestamp":1498867200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100012166","name":"973 Program","doi-asserted-by":"crossref","award":["No. 2014CB340701"],"award-info":[{"award-number":["No. 2014CB340701"]}],"id":[{"id":"10.13039\/501100012166","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100001809","name":"NSFC","doi-asserted-by":"crossref","award":["No. 91418204","No. 61625206","No. 61532019","No. 61472473"],"award-info":[{"award-number":["No. 91418204","No. 61625206","No. 61532019","No. 61472473"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,7]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we propose a general compositional approach for modelling and verification of stochastic hybrid systems (SHSs). We extend Hybrid CSP (HCSP), a very expressive process algebra-like formal modeling language for hybrid systems, by introducing probability and stochasticity to model SHSs, which we call stochastic HCSP (SHCSP). Especially, non-deterministic choice is replaced by probabilistic choice, ordinary differential equations are replaced by stochastic differential equations (SDEs), and communication interrupts are generalized by communication interrupts with weights. We extend Hybrid Hoare Logic to specify and reason about SHCSP processes: On the one hand, we introduce the probabilistic formulas for describing probabilistic states, and on the other hand, we propose the notions of local stochastic differential invariants for characterizing SDEs and global loop invariants for repetition. Throughout the paper, we demonstrate our approach by an aircraft running example.<\/jats:p>","DOI":"10.1007\/s00165-017-0421-7","type":"journal-article","created":{"date-parts":[[2017,2,23]],"date-time":"2017-02-23T12:52:36Z","timestamp":1487854356000},"page":"751-775","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2798-2660","authenticated-orcid":false,"given":"Shuling","family":"Wang","sequence":"first","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Building 5, Software Park, No. 4, South 4th Street, Zhongguancun, Haidian District, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Building 5, Software Park, No. 4, South 4th Street, Zhongguancun, Haidian District, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[{"name":"State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Building 5, Software Park, No. 4, South 4th Street, Zhongguancun, Haidian District, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1137\/S0363012995279985"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2008.03.027"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2015.02.003"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bujorianu ML Lygeros J (2006) Toward a general theory of stochastic hybrid systems. In: Lecture notes in control and information sciences (LNCIS) vol 337 pp 3\u201330","DOI":"10.1007\/11587392_1"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bujorianu Manuela L Lygeros John Bujorianu Marius C (2005) Bisimulation for general stochastic hybrid systems. In: HSCC\u201905 LNCS vol 3414 pp 198\u2013214","DOI":"10.1007\/978-3-540-31954-2_13"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: HSCC\u201904 LNCS vol 2993 pp 234\u2013249","DOI":"10.1007\/978-3-540-24743-2_16"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Chen M Fr\u00e4nzle M Li Y Mosaad PN Zhan N (2016) Validated simulation-based verification of delayed differential dynamics. In: FM\u201916 LNCS vol 9995 pp 137\u2013154","DOI":"10.1007\/978-3-319-48989-6_9"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.262058"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Fr\u00e4nzle M Hahn EM Hermanns H Wolovick N Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: HSCC\u201911 pp 43\u201352. ACM","DOI":"10.1145\/1967701.1967710"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Goubault E Jourdan J-H Putot S Sankaranarayanan S (2014) Finding non-polynomial positive invariants and Lyapunov functions for polynomial systems through Darboux polynomials. In: ACC 2014 pp 3571\u20133578","DOI":"10.1109\/ACC.2014.6859330"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.peva.2013.11.004"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Gulwani S Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A Malik S (eds) CAV\u201908 LNCS vol 5123 pp 190\u2013203. Springer Berlin","DOI":"10.1007\/978-3-540-70545-1_18"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Hartog JI (1999) Verifying probabilistic programs using a hoare like logic. In: ASIAN 1999 LNCS vol 1742 pp 113\u2013125","DOI":"10.1007\/3-540-46674-6_11"},{"key":"e_1_2_1_2_14_2","unstructured":"He J (1994) From CSP to hybrid systems. In: A classical mind essays in Honour of C.A.R. Hoare. Prentice Hall International (UK) Ltd London pp 171\u2013189"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA (July 1996) The theory of hybrid automata. In: LICS\u201996 pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0167-z"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Hahn EM Hermanns H Wachter B Zhang L (2010) PASS: abstraction refinement for infinite probabilistic models. In: TACAS\u201910 LNCS vol 6015 pp 353\u2013357","DOI":"10.1007\/978-3-642-12002-2_30"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Hu J Lygeros J Sastry S (2002) Towards a theory of stochastic hybrid systems. In: HSCC\u201902 LNCS vol 1790 pp 160\u2013173","DOI":"10.1007\/3-540-46430-1_16"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576\u2013580","DOI":"10.1145\/363235.363259"},{"key":"e_1_2_1_2_20_2","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall Englewood Cliffs"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M Norman G Parker D Qu H (2010) Assume-guarantee verification for probabilistic systems. In: TACAS 2010 LNCS vol 6015 pp 23\u201337","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Liu J Lv J Quan Z Zhan N Zhao H Zhou C Zou L (2010) A calculus for hybrid CSP. In: APLAS\u201910 LNCS vol 6461 pp 1\u201315","DOI":"10.1007\/978-3-642-17164-2_1"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Liu J Zhan N Zhao H Zou L (2015) Abstraction of elementary hybrid systems by variable transformation. In: FM 2015 LNCS vol 9109. Springer International Publishing pp 360\u2013377","DOI":"10.1007\/978-3-319-19249-9_23"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01213492"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Meseguer J Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: HSCC\u201906 LNCS vol 3927 pp 460\u2013475","DOI":"10.1007\/11730637_35"},{"volume-title":"Stochastic differential equations: an introduction with applications","year":"2007","author":"\u00d8ksendal B","key":"e_1_2_1_2_27_2"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Platzer A Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. In: CAV 2008 LNCS vol 5123 pp 176\u2013189","DOI":"10.1007\/978-3-540-70545-1_17"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Prandini M Hu J (2008) Application of reachability analysis for stochastic hybrid systems to aircraft conflict prediction. In: 47th IEEE conference on decision and control (CDC). IEEE pp 4036 \u2013 4041","DOI":"10.1109\/CDC.2008.4739248"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.902736"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn070"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: CADE\u201911 LNCS vol 6803 pp 446\u2013460","DOI":"10.1007\/978-3-642-22438-6_34"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Peng Y Wang S Zhan N Zhang L (2015) Extending hybrid CSP with probability and stochasticity. In: SETTA\u201915 LNCS vol 9409 pp 87\u2013102","DOI":"10.1007\/978-3-319-25942-0_6"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Rebiha R Matringe N Moura AV (2012) Transcendental inductive invariants generation for non-linear differential and hybrid systems. In: HSCC 2012 New York NY USA. ACM pp 25\u201334","DOI":"10.1145\/2185632.2185640"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S (2010) Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC\u201910 New York NY USA. ACM pp 221\u2013230","DOI":"10.1145\/1755952.1755984"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Sproston J (2000) Decidable model checking of probabilistic hybrid automata. In: Formal techniques in real-time and fault-tolerant systems LNCS vol 1926 pp 31\u201345","DOI":"10.1007\/3-540-45352-0_5"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan S Sipma HB Manna Z (2004) Constructing invariants for hybrid systems. In: Alur R Pappas GJ (eds) HSCC\u201904 LNCS vol 2993 pp 539\u2013554","DOI":"10.1007\/978-3-540-24743-2_36"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0013091506000988"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Wang S Zhan N Guelev D (2012) An assume\/guarantee based compositional calculus for hybrid CSP. In: Agrawal M Cooper SB Li A (eds) TAMC 2012 LNCS vol 7287. Springer Berlin pp 72\u201383","DOI":"10.1007\/978-3-642-29952-0_13"},{"issue":"1","key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1145\/2629424","article-title":"Exact safety verification of hybrid systems based on bilinear SOS representation","volume":"14","author":"Yang Z","year":"2015","journal-title":"ACM Trans Embed Comput Syst"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Zou L Fr\u00e4nzle M Zhan N Mosaad PN (2015) Automatic verification of stability and safety for delay differential equations. In: CAV\u201915 LNCS vol 9207 pp 338\u2013355","DOI":"10.1007\/978-3-319-21668-3_20"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0195-3"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Zhang L She Z Ratschan S Hermanns H Hahn EM (2010) Safety verification for probabilistic hybrid systems. In: CAV\u201910 LNCS vol 6174 pp 196\u2013211","DOI":"10.1007\/978-3-642-14295-6_21"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Zhou C Wang J Ravn AP (1996) A formal description of hybrid systems. In: Hybrid systems III LNCS vol 1066 pp 511\u2013530","DOI":"10.1007\/BFb0020972"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Zhan N Wang S Zhao H (2013) Formal modelling analysis and verification of hybrid systems. In: Unifying theories of programming and formal engineering methods LNCS vol 8050 pp 207\u2013281","DOI":"10.1007\/978-3-642-39721-9_5"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-017-0421-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0421-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-017-0421-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-017-0421-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T16:34:14Z","timestamp":1750005254000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-017-0421-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2017,7]]}},"alternative-id":["10.1007\/s00165-017-0421-7"],"URL":"https:\/\/doi.org\/10.1007\/s00165-017-0421-7","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,7]]}}}