Hybrid formal verification of greenhouse temperature-humidity system based on MLD model

摘要

In this paper, based on mixed logical dynamical (MLD) model, the hybrid formal verification problem of greenhouse temperature-humidity system is investigated. First, the set of desired states is defined as reach set, and the greenhouse temperature-humidity system is modeled in the MLD form. Then the operation safety problems of the greenhouse temperature-humidity system are transformed into hybrid formal verification problems. The reachable sets are computed by multi-parametric toolbox (MPT). At last, the simulation result demonstrates that the greenhouse temperature-humidity system can be driven to desired reach set with proper control actions calculated by hybrid formal verification algorithm. This paper illustrates the effectiveness of the hybrid formal verification method and provides a novel approach to handle the operation safety problems of greenhouse temperature-humidity system.