In this paper we propose a formal, model-checking based procedure to evaluate the survivability of fluid critical infrastructures. To do so, we introduce the Stochastic Time Logic (STL), which allows to precisely express intricate state-based and until-based properties for an important class of hybrid Petri nets. We present an efficient model checking procedure which recursively traverses the underlying state-space of the hybrid Petri net model, and identifies those regions (subsets of the discrete-continuous state space) that satisfy STL formulae. A case study studying the survivability of a water refinery and distribution plant shows the feasibility of our approach.
- Survivability evaluation
- Fluid critical infrastructures
- Model Checking
- Hybrid Petri nets
Ghasemieh, H., Remke, A. K. I., & Haverkort, B. R. H. M. (2013, Dec). Survivability evaluation of fluid critical infrastructures using hybrid Petri nets. USA: IEEE Computer Society. https://doi.org/10.1109/PRDC.2013.34