More Web Proxy on the site http://driver.im/

research-article

Open access

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems

Authors:

Lijun ZhangAuthors Info & Claims

Formal Aspects of Computing, Volume 29, Issue 4

Pages 751 - 775

https://doi.org/10.1007/s00165-017-0421-7

Published: 01 July 2017 Publication History

Abstract

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.

References

References

[1]

Altman E and Gaitsgory V Asymptotic optimization of a nonlinear hybrid system governed by a Markov decision process SIAM J Control Optim 1997 35 6 2070-2085

Digital Library

[2]

Abate A, Prandini M, Lygeros J, and Sastry S Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems Automatica 2008 44 11 2724-2734

Digital Library

[3]

Banach R, Butler M, Qin S, Verma N, and Zhu H Core hybrid event-B I: single hybrid event-B machines Sci Comput Program 2015 105 92-123

Digital Library

[4]

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–30

[5]

Bujorianu Manuela L, Lygeros John, Bujorianu Marius C (2005) Bisimulation for general stochastic hybrid systems. In: HSCC’05, LNCS, vol 3414, pp 198–214

[6]

Bujorianu ML (2004) Extended stochastic hybrid systems and their reachability problem. In: HSCC’04, LNCS, vol 2993, pp 234–249

[7]

Chen M, Fränzle M, Li Y, Mosaad PN, Zhan N (2016) Validated simulation-based verification of delayed differential dynamics. In: FM’16, LNCS, vol 9995, pp 137–154

[8]

Castelan EB and Hennet JC On invariant polyhedra of continuous-time linear systems IEEE Trans Autom Control 1993 38 11 1680-1685

[9]

Fränzle M, Hahn EM, Hermanns H, Wolovick N, Zhang L (2011) Measurability and safety verification for stochastic hybrid systems. In: HSCC’11, pp 43–52. ACM

[10]

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–3578

[11]

Gretz F, Katoen J-P, and McIver A Operational versus weakest pre-expectation semantics for the probabilistic guarded command language Perform Eval 2014 73 110-132

Digital Library

[12]

Gulwani S, Tiwari A (2008) Constraint-based approach for analysis of hybrid systems. In: Gupta A, Malik S (eds) CAV’08, LNCS, vol 5123, pp 190–203. Springer, Berlin

[13]

Hartog JI (1999) Verifying probabilistic programs using a hoare like logic. In: ASIAN 1999, LNCS, vol 1742, pp 113–125

[14]

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–189

[15]

Henzinger TA (July 1996) The theory of hybrid automata. In: LICS’96, pp 278–292

[16]

Hahn EM, Hartmanns A, Hermanns H, and Katoen J.-P. A compositional modelling and analysis framework for stochastic hybrid systems Form Methods Syst Des 2013 43 2 191-232

Digital Library

[17]

Hahn EM, Hermanns H, Wachter B, Zhang L (2010) PASS: abstraction refinement for infinite probabilistic models. In: TACAS’10, LNCS, vol 6015, pp 353–357

[18]

Hu J, Lygeros J, Sastry S (2002) Towards a theory of stochastic hybrid systems. In: HSCC’02, LNCS, vol 1790, pp 160–173

[19]

Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580

[20]

Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs

[21]

Kwiatkowska M, Norman G, Parker D, Qu H (2010) Assume-guarantee verification for probabilistic systems. In: TACAS 2010, LNCS, vol 6015, pp 23–37

[22]

Liu J, Lv J, Quan Z, Zhan N, Zhao H, Zhou C, Zou L (2010) A calculus for hybrid CSP. In: APLAS’10, LNCS, vol 6461, pp 1–15

[23]

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–377

[24]

Morgan C, McIver A, and Seidel K Probabilistic predicate transformers ACM Transactions on Programming Languages and Systems, 1996 18 3 325-353

Digital Library

[25]

Morgan C, McIver A, Seidel K, and Sanders JW Refinement-oriented probability for CSP Form Asp Comput 1996 8 6 617-647

Digital Library

[26]

Meseguer J, Sharykin R (2006) Specification and analysis of distributed object-based stochastic hybrid systems. In: HSCC’06, LNCS, vol 3927, pp 460–475

[27]

Øksendal B Stochastic differential equations: an introduction with applications 2007 Berlin Springer

[28]

Platzer A, Clarke EM (2008) Computing differential invariants of hybrid systems as fixedpoints. In: CAV 2008, LNCS, vol 5123, pp 176–189

[29]

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 – 4041

[30]

Prajna S, Jadbabaie A, and Pappas GJ A framework for worst-case and stochastic safety verification using barrier certificates IEEE Trans Autom Control 2007 52 8 1415-1428

[31]

Platzer A Differential-algebraic dynamic logic for differential-algebraic programs J Log Comput 2010 20 1 309-352

Digital Library

[32]

Platzer A (2011) Stochastic differential dynamic logic for stochastic hybrid programs. In: CADE’11, LNCS, vol 6803, pp 446–460

[33]

Peng Y, Wang S, Zhan N, Zhang L (2015) Extending hybrid CSP with probability and stochasticity. In: SETTA’15, LNCS, vol 9409, pp 87–102

[34]

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–34

[35]

Sankaranarayanan S (2010) Automatic invariant generation for hybrid systems using ideal fixed points. In: HSCC’10, New York, NY, USA. ACM, pp 221–230

[36]

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–45

[37]

Sankaranarayanan S, Sipma HB, Manna Z (2004) Constructing invariants for hybrid systems. In: Alur R, Pappas GJ (eds) HSCC’04, LNCS, vol 2993, pp 539–554

[38]

Tang X and Zou X Global attractivity in a predator-prey system with pure delays Proc Edinburgh Math Soc 2008 51 495-508

[39]

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–83

[40]

Yang Z, Lin W, and Wu M Exact safety verification of hybrid systems based on bilinear SOS representation ACM Trans Embed Comput Syst 2015 14 1 16-11619

Digital Library

[41]

Zou L, Fränzle M, Zhan N, Mosaad PN (2015) Automatic verification of stability and safety for delay differential equations. In: CAV’15, LNCS, vol 9207, pp 338–355

[42]

Zuliani P, Platzer A, and Clarke EM Bayesian statistical model checking with application to stateflow/simulink verification Form Methods Syst Des 2013 43 2 338-367

Digital Library

[43]

Zhang L, She Z, Ratschan S, Hermanns H, Hahn EM (2010) Safety verification for probabilistic hybrid systems. In: CAV’10, LNCS, vol 6174, pp 196–211

[44]

Zhou C, Wang J, Ravn AP (1996) A formal description of hybrid systems. In: Hybrid systems III, LNCS, vol 1066, pp 511–530

[45]

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–281

Cited By

Maximova MSchneider SGiese H(2023)Compositional Analysis of Probabilistic Timed Graph Transformation SystemsFormal Aspects of Computing10.1145/357278235:3(1-79)Online publication date: 13-Sep-2023
https://dl.acm.org/doi/10.1145/3572782
Xu XTalpin JWang SZhan BZhan N(2023)Semantics Foundation for Cyber-physical Systems Using Higher-order UTPACM Transactions on Software Engineering and Methodology10.1145/351719232:1(1-48)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3517192
Lanotte RTini S(2021)A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spacesTheoretical Computer Science10.1016/j.tcs.2020.12.045869(29-61)Online publication date: May-2021
https://doi.org/10.1016/j.tcs.2020.12.045
Show More Cited By

Index Terms

A Compositional Modelling and Verification Framework for Stochastic Hybrid Systems

Index terms have been assigned to the content through auto-classification.

Recommendations

Abstraction-based Synthesis of Stochastic Hybrid Systems
HSCC '24: Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control

In this work, we develop a framework for formally constructing finite abstractions, also known as finite Markov decision processes (MDPs), for continuous-space stochastic hybrid systems. These complex systems encompass both continuous dynamics, ...
Stability analysis for stochastic hybrid systems

This survey addresses stability analysis for stochastic hybrid systems (SHS), which are dynamical systems that combine continuous change and instantaneous change and that also include random effects. We re-emphasize the common features found in most of ...
Limit behavior of the hybrid approximation of stochastic process algebras
ASMTA'10: Proceedings of the 17th international conference on Analytical and stochastic modeling techniques and applications

We investigate the limit behavior of a class of stochastic hybrid systems obtained by hybrid approximation of Stochastic Concurrent Constraint Programming (sCCP). We prove that a sequence of Continuous Time Markov Chain (CTMC), constructed from sCCP ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Aspects of Computing

Formal Aspects of Computing Volume 29, Issue 4

Jul 2017

192 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

© British Computer Society 2017.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 July 2017

Accepted: 08 December 2016

Received: 28 March 2016

Published in FAC Volume 29, Issue 4

Author Tags

Qualifiers

Research-article

Funding Sources

973 Program
NSFC

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
74
Total Downloads

Downloads (Last 12 months)44
Downloads (Last 6 weeks)7

Reflects downloads up to 20 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Maximova MSchneider SGiese H(2023)Compositional Analysis of Probabilistic Timed Graph Transformation SystemsFormal Aspects of Computing10.1145/357278235:3(1-79)Online publication date: 13-Sep-2023
https://dl.acm.org/doi/10.1145/3572782
Xu XTalpin JWang SZhan BZhan N(2023)Semantics Foundation for Cyber-physical Systems Using Higher-order UTPACM Transactions on Software Engineering and Methodology10.1145/351719232:1(1-48)Online publication date: 13-Feb-2023
https://dl.acm.org/doi/10.1145/3517192
Lanotte RTini S(2021)A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spacesTheoretical Computer Science10.1016/j.tcs.2020.12.045869(29-61)Online publication date: May-2021
https://doi.org/10.1016/j.tcs.2020.12.045
Lanotte RMerro MTini S(2021)A probabilistic calculus of cyber-physical systemsInformation and Computation10.1016/j.ic.2020.104618279(104618)Online publication date: Aug-2021
https://doi.org/10.1016/j.ic.2020.104618
Xue BFranzle MZhan NBogomolov SXia B(2020)Safety Verification for Random Ordinary Differential EquationsIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2020.301313539:11(4090-4101)Online publication date: Nov-2020
https://doi.org/10.1109/TCAD.2020.3013135
Lanotte RTini S(2018)Weak Bisimulation Metrics in Models with Nondeterminism and Continuous State SpacesTheoretical Aspects of Computing – ICTAC 201810.1007/978-3-030-02508-3_16(292-312)Online publication date: 15-Oct-2018
https://doi.org/10.1007/978-3-030-02508-3_16
Ding JChen XWang R(2017)A Compositional Analysis Method for Petri-Net ModelsIEEE Access10.1109/ACCESS.2017.27728295(27599-27610)Online publication date: 2017
https://doi.org/10.1109/ACCESS.2017.2772829

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents