Parametric multisingular hybrid Petri nets: Formal definitions and analysis techniques

Silva, 2004, On fluidification of Petri nets: from discrete to hybrid and continuous models, Annu. Rev. Control, 28, 253, 10.1016/j.arcontrol.2004.05.002 Recalde, 2010, Continuous Petri nets: expressive power and decidability issues, Int. J. Found. Comput. Sci., 21, 235, 10.1142/S0129054110007222 Henzinger, 1996, The theory of hybrid automata, 278 Alur, 1995, The algorithmic analysis of hybrid systems, Theor. Comput. Sci., 138, 3, 10.1016/0304-3975(94)00202-T Alur, 1994, A theory of timed automata, Theor. Comput. Sci., 126, 183, 10.1016/0304-3975(94)90010-8 Henzinger, 1994, Symbolic model checking for real-time systems, Inf. Comput., 111, 193, 10.1006/inco.1994.1045 David, 2005 Lime, 2009, Formal verification of real-time systems with preemptive scheduling, Real-Time Syst., 41, 118, 10.1007/s11241-008-9059-0 David, 1990, Autonomous and timed continuous Petri nets, 367 Balduzzi, 2001, Decidability results in first-order hybrid Petri nets, Discrete Event Dyn. Syst., 11, 41, 10.1023/A:1008383031624 David, 2001, On hybrid Petri nets, Discrete Event Dyn. Syst., 11, 9, 10.1023/A:1008330914786 Bérard, 2005, Comparison of the expressiveness of timed automata and time Petri nets, 211 Srba, 2008, Comparing the expressiveness of timed automata and timed extensions of Petri nets, 15 Berthomieu, 2006, Bridging the gap between timed automata and bounded time Petri nets, 82 Bouyer, 2008, Timed Petri nets and timed automata: on the discriminating power of zeno sequences, Inf. Comput., 206, 73, 10.1016/j.ic.2007.10.004 Sava, 2001, Combining hybrid Petri nets and hybrid automata, IEEE Trans. Robot. Autom., 17, 670, 10.1109/70.964667 Cassez, 2006, Structural translation from time Petri nets to timed automata, J. Syst. Softw., 79, 1456, 10.1016/j.jss.2005.12.021 Motallebi, 2013, Translation from multisingular hybrid Petri nets to multisingular hybrid automata, J. Fundam. Inform., 130, 1 Ghomri, 2005, Structural and hierarchical translation of hybrid Petri nets in hybrid automata Motallebi, 2012, Modelling and verification of hybrid dynamic systems using multisingular hybrid Petri nets, Theor. Comput. Sci. (TCS), 446, 48, 10.1016/j.tcs.2012.05.023 Traonouez, 2009, Parametric model-checking of stopwatch Petri nets, J. Univers. Comput. Sci., 15, 3273 Henzinger, 1997, HyTech: a model checker for hybrid systems, 460 Henzinger, 1998, What's decidable about hybrid automata?, J. Comput. Syst. Sci., 57, 94, 10.1006/jcss.1998.1581 Aceto, 2003, The power of reachability testing for timed automata, Theor. Comput. Sci., 300, 411, 10.1016/S0304-3975(02)00334-1 Bozga, 1998, Kronos: a model checking tool for real-time systems, 546 McManis, 1994, Suspension automata: a decidable class of hybrid automata, 105 Fersman, 2007, Task automata: schedulability, decidability and undecidability, Inf. Comput., 205, 1149, 10.1016/j.ic.2007.01.009 Cassez, 2000, The impressive power of stopwatches, 138 Bérard, 2009, Interrupt timed automata, 197 Bérard, 2012, Interrupt timed automata: verification and expressiveness, Form. Methods Syst. Des., 40, 41, 10.1007/s10703-011-0140-2 Lime, 2006, Model checking of time Petri nets using the state class timed automaton, Discrete Event Dyn. Syst., 16, 179, 10.1007/s10626-006-8133-9 Okawa, 1996, Schedulability verification of real-time systems with extended time Petri nets, Int. J. Mini Microcomput., 18, 148 Horton, 1998, Fluid stochastic Petri nets: theory, applications, and solution techniques, Eur. J. Oper. Res., 105, 184, 10.1016/S0377-2217(97)00028-3 Ciardo, 1999, Discrete-event simulation of fluid stochastic Petri nets, IEEE Trans. Softw. Eng., 25, 207, 10.1109/32.761446 Gribaudo, 2001, Fluid stochastic Petri nets augmented with flush-out arcs: modelling and analysis, Discrete Event Dyn. Syst., 11, 97, 10.1023/A:1008339216603 Ghasemieh, 2012, Region-based analysis of hybrid Petri nets with a single general one-shot transition, 139 Gribaudo, 2010, Hybrid Petri nets with general one-shot transitions for dependability evaluation of fluid critical infrastructures, 84 David, 1987, Continuous Petri nets, 275 Hanzálek, 2003, Continuous Petri nets and polytopes, 1513 Alur, 1993, Parametric real-time reasoning, 592 Hune, 2002, Linear parametric model checking of timed automata, J. Log. Algebr. Program., 52–53, 183, 10.1016/S1567-8326(02)00037-1 Bozzelli, 2009, Decision problems for lower/upper bound parametric timed automata, Form. Methods Syst. Des., 35, 121, 10.1007/s10703-009-0074-0 Doyen, 2007, Robust parametric reachability for timed automata, Inf. Process. Lett., 102, 208, 10.1016/j.ipl.2006.11.018 Jovanovic, 2013, Integer parameter synthesis for timed automata, 401 Bruyere, 2007, Real-time model-checking: parameters everywhere, Log. Methods Comput. Sci., 3, 1, 10.2168/LMCS-3(1:7)2007 Bagnara, 2004, The Parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Sci. Comput. Program., 72, 3 Wang, 1996, Parametric timing analysis for real-time systems, Inf. Comput., 130, 131, 10.1006/inco.1996.0086 Bérard, 2013, Parametric interrupt timed automata, 24 Virbitskaite, 1999, Parametric behavior analysis for time Petri nets, 134 Roux, 2004, Time Petri nets with inhibitor hyperarcs. Formal semantics and state space computation, 371 Lime, 2009, Romeo: a parametric model-checker for Petri nets with stopwatches, 54 Knapik, 2012, Bounded model checking for parametric timed automata, 141 Bornot, 1997, Relating time progress and deadlines in hybrid systems, 286 Bornot, 1997, Modeling urgency in timed systems, 103 Ajmone Marsan, 1995 Alur, 1993, Model-checking in dense real-time, Inf. Comput., 104, 2, 10.1006/inco.1993.1024 Baier, 2007 Lime, 2009, Romeo: a parametric model-checker for Petri nets with stopwatches, 54 Bagnara, 2002, Possibly not closed convex polyhedra and the Parma polyhedra library, 213 Le Boudec, 2001, Network Calculus – a Theory of Deterministic Queuing Systems for the Internet, vol. 2050 Thiele, 2000, Real-time calculus for scheduling hard real-time systems, 101 Chakraborty, 2003, A general framework for analysing system properties in platform-based embedded system designs, 10190 Phan, 2008, A multi-mode real-time calculus, 59 Chakraborty, 2005, Event count automata: a state-based model for stream processing systems, 87 Babcock, 2004, Operator scheduling in data stream systems, Int. VLDB J., 13, 333, 10.1007/s00778-004-0132-6 Maxiaguine, 2004, Rate analysis for streaming applications with on-chip buffer constraints, 131 Geilen, 2005, Minimising buffer requirements of synchronous dataflow graphs with model checking, 819