We apply reinforcement learning to approximate the optimal probability that a stochastic hybrid system satisfies a temporal logic formula. We consider systems with (non)linear continuous dynamics, random events following general continuous probability distributions, and discrete nondeterministic choices. We present a discretized view of states to the learner, but simulate the continuous system. Once we have learned a near-optimal scheduler resolving the choices, we use statistical model checking to estimate its probability of satisfying the formula. We implemented the approach using Q-learning in the tools HYPEG and modes, which support Petri net- and hybrid automata-based models, respectively. Via two case studies, we show the feasibility of the approach, and compare its performance and effectiveness to existing analytical techniques for a linear model. We find that our new approach quickly finds near-optimal prophetic as well as non-prophetic schedulers, which maximize or minimize the probability that a specific signal temporal logic property is satisfied.

Nondeterminism occurs naturally in Petri nets whenever multiple events are enabled at the same time. Traditionally, it is resolved at specification time using probability weights and priorities. In this paper, we focus on model checking for hybrid Petri nets with an arbitrary but finite number of stochastic firings (HPnGs) while preserving the inherent nondeterminism as a first-class modelling and analysis feature. We present two algorithms to compute optimal non-prophetic and prophetic schedulers. The former can be applied to all HPnG models while the latter is only applicable if information on the firing times of general transitions is specifically encoded in the model. Both algorithms make use of recent work on the parametric location tree, which symbolically unfolds the state space of an HPnG. A running example illustrates the approach and confirms the feasibility of the presented algorithm.

Supervisory Control and Data Acquisition (SCADA) systems monitor and control electric power distribution. Recent history has shown that cyber-attacks pose a tremendous risk for the economy and safety of modern countries. This paper introduces an architecture and a prototype implementation for a process-aware, network-based Intrusion Detection System (IDS) to secure control networks in the domain of power distribution. Based on a recently proposed process model, the system continuously assesses the local physical process and all control commands with regard to consistency and safety of the underlying physical process. Its detection capabilities focus on process-based attacks like manipulated control commands, which appear legitimate to traditional IDS but might nevertheless have devastating effects on the power distribution. The architecture separates the evaluation part from the traffic processing, which ensures extensibility and scalability. The developed implementation has been successfully tested at a Dutch power distribution substation. Its detection performance is characterized by a very low miss rate and high precision.

Hybrid Petri nets with general transitions (HPnGs) provide a formalism for modeling safety-critical systems and evaluating their dependability with means of model checking. HPnGs form a restricted subclass of Stochastic Hybrid Automata and allow discrete, continuous and stochastic variables. Previously, discrete-event simulation and Statistical Model Checking (SMC) have been used to overcome the restrictions of existing analytical approaches, e.g., to a limited number of random variables. Also when simulating, the evolution of continuous variables has been restricted to piecewise-linear trajectories, where derivatives do not change between two events. Here, we extend the modeling formalism, the simulation and SMC approach to variables with a non-linear continuous evolution. The core idea of this extension lies in transforming the input system into a so-called second-order quantized state system. A case study on the Kinetic Battery Model validates our approach by comparing results to those obtained by Matlab.

The modeling formalism of hybrid Petri nets allows investigating the dependability of e.g. critical infrastructures with hybrid characteristics. Hybrid Petri nets can model random delays with so-called general transitions. Approaches for analyzing such Petri nets are available for models with one or two general transitions, which change the discrete marking of the system by firing only once. We extend the formalism to more general transitions that possibly fire multiple times. This work provides a definition of the probability space for the evolution of hybrid Petri nets over time and presents an efficient approach to discrete-event simulation. Statistical Model Checking techniques are introduced to verify complex properties on hybrid Petri nets. The presented methods are implemented in Java and we show their feasibility in a case study that also serves to validate our results.

The number of local power generation units, such as photovoltaic panels (PV), increased enormously in recent years. Their production patterns are highly variable and depend on the current weather. The resulting fluctuation in production poses a major challenge to the stability of the power grid. The use of local energy storages may help to ensure that the locally produced power is fed into the grid in a grid-convenient way. It may also help clients to increase the self-use of locally generated power and to increase the so-called survivability of their homes in the presence of a power outage. This paper compares the interest of the power operator, i.e. grid-convenience with the interests of the user, i.e. self-use and survivability for different battery management strategies: i) direct loading, ii) delayed loading and iii) peak shaving. We use a Hybrid Petri Net model with one stochastic variable (HPnG) to model smart homes with local power generation, local storage and different battery management strategies in the presence of power outages. Recent algorithms for analyzing and model checking HPnGs enable the computation of the above mentioned measures of interest. We are able to show that whenever good predictions of production and demand exist, grid-convenience does not decrease the survivability and the self-use of a smart home.

The use of renewable energy in houses and neighbourhoods is very much governed by national legislation and has recently led to enormous changes in the energy market and poses a serious threat to the stability of the grid at peak production times. One of the approaches towards a more balanced grid is, e.g., taken by the German government by subsidizing local storage for solar power. While the main interest of the energy operator and the government is to balance the grid, thereby ensuring its stability, the main interest of the client is twofold: the total cost for electricity should be as low as possible and the house should be as resilient as possible in the presence of power outages. Using local battery storage can help to overcome the effects of power outages. However, the resulting resilience highly depends on the battery usage strategy employed by the controller, taking into account the state of charge of the battery. We present a Hybrid Petri net model of a house (that is mainly powered by solar energy) with a local storage unit, and analyse the impact of different battery usage strategies on its resilience for different production and consumption patterns. Our analysis shows that there is a direct relationship between resilience and flexibility, since increased resilience, i.e., reserving battery capacity for backup, decreases the flexibility of the storage unit.

Recently the mean-field method has been adopted for analysing systems consisting of a large number of interacting objects in computer science, biology, chemistry, etc. It allows for a quick and accurate analysis of such systems, while avoiding the state-space explosion problem. So far, the method has primarily been used for performance evaluation. In this paper, we use the mean-field method for model-checking. We define and motivate a logic MF-CSL for describing properties of systems composed of many identical interacting objects. The proposed logic allows describing both properties of the overall system and of a random individual object. Algorithms to check the satisfaction relation for all MF-CSL operators are proposed. Furthermore, we explain how the set of all time instances that fulfill a given MF-CSL formula for a certain distribution of objects can be computed.

In process industries wired supervisory and control networks are more and more replaced by wireless systems. Wireless communication inevitably introduces time delays and message losses, which may degrade the system reliability and performance. WirelessHART, as the first international standard for wireless process supervision and control has received notable academic attention. This paper models WirelessHART networks with link failures using Discrete-time Markov chains and evaluates the network performance in a typical WirelessHART environment with respect to delay and reachability. The evaluation shows that although the performance of WirelessHART is influenced by several factors, it is capable to deliver reliable service in typical industrial environments. The proposed model can also be used to predict path performance and to provide routing suggestions.

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.

The performance and dependability of critical infrastructures, such as water-treatment facilities is essential. In this paper we use various performance and dependability measures to analyze a simplified model of a water treatment facility. Building on the existing architectural framework Arcade a model is derived in XML format and then automatically mapped to the model checker PRISM. Using the stochastic model checking capabilities that PRISM offers, we compare different repair strategies, with respect to their costs, system reliability, availability and survivability. For this case study we conclude that using non-preemtive priority scheduling with additional repair crews is the best choice with respect to performance, dependability and costs.