Hybrid State Petri Nets which Have the Analysis Power of Stochastic Hybrid Systems and the Formal Verification Power of Automata
Mariken H.C., Henk A.P. · InTech eBooks · 2010
QWURGXFWLRQFor a large range of complex applications, governments and industries invest in the development of innovative new systems existing of many distributed components that interact in a dynamic way with many uncertainties.Before any such system can be introduced into practice, an evaluation needs to have shown that both the system and the way it is used in its new context realizes the applicable objectives.If the new complex system is in its interactions similar to a previous system, such investigation can be done by analysis judgement of capable and experienced experts who judge local behaviour and implicitly assume that the interactions are working as before.If the complex system is very different from the old system, then this expert judgement approach falls short.A valuable alternative is to develop a mathematical model that incorporates the interactions, analyse this model, mobilise domain experts to evaluate where the model is representative for reality and where it needs improvement, and learn to understand how the real system works by learning how the model works.This requires a growing need for modelling and analysis of stochastic hybrid systems.Petri nets, e.g.(David & Alla, 1994), have shown to be useful for developing models of various complex applications.Typical Petri net features are concurrency and synchronisation mechanism, hierarchical and modular construction, and natural expression of causal dependencies, in combination with graphical and equational representation.Numerous extensions to the basic formalism have been developed that combine different modelling features in an integrated way, including various hybrid state Petri net versions, e.g.(Giua, 1999), which combine discrete and continuous system aspects.As a powerful class of models that support stochastic analysis, (Davis, 1984;1993) introduced piecewise deterministic Markov processes (PDPs) as the most general class of continuous-time hybrid state Markov processes which include both discrete and continuous processes, except diffusion.In (Bujorianu & Lygeros, 2003;Hu et al., 2000) the PDPs have been defined as stochastic hybrid automata.Subsequently, diffusion by means of Brownian motion has been incorporated (Bujorianu & Lygeros, 2006).This way, a formal connection is established between stochastic hybrid processes that are supported by powerful stochastic analysis tools (Davis, 1993;Elliott, 1982;Elliott et al., 1995) and the automata formalism to develop formal verification tools (Frehse, 2008;Kwiatkowska et al., 2004;Labinaz et al., 1997). www.intechopen.com 2GVTK 0GVU #RRNKECVKQPU How to referenceIn order to correctly reference this scholarly work, feel free to copy and paste the following: Mariken H.C. Everdij and Henk A.P.