Abstract Effective water management in underground mining requires maintaining safe reservoir levels while minimizing the high energy costs of continuous pumping. Although flexible electricity pricing enables cost-aware operation, traditional threshold-based controllers cannot exploit this flexibility efficiently. This paper presents an industrial case study on efficient mine dewatering using reinforcement-learning-based control synthesized with the Uppaal Stratego framework. A baseline threshold controller is first implemented, followed by a reinforcement-learning controller trained on forecast inflows and day-ahead electricity prices to minimize pumping costs while limiting pump switching. To ensure safety during learning without distorting the optimization objective, we introduce a pre-shield that blocks unsafe transitions. We formally show that this pre-shield is maximally permissive with respect to a monotonicity safety objective. Simulation results demonstrate that the learning-based strategy reduces total energy consumption by up to 40% compared to threshold-based control, while maintaining safe operation in all scenarios.

Digital Twins (DTs) are virtual representations of physical products in many dimensions, such as geometry and behaviour. As a backbone of Industry 4.0, DTs help interpret and even predict the behaviour of physical processes, provide a virtual testbed for maintenance and upgrade, and enable automatic decision-making supported by artificial intelligence. Despite the promising future, challenges exist, such as the absence of a framework that facilitates the development and application of DTs in industrial contexts. We propose a service-oriented architecture (SOA) DT framework for dynamic and robust distributed systems. The framework contains two types of services. One includes the services provided to the users and is supported by an orchestration mechanism to ensure a quality of service (QoS). The other one refers to the common functions of all DTs. Further, we describe the DT-based decision-making enabled by our QoS-oriented learning of the framework and a Hoare-logic-based verification of QoS.