2015/06/05 by Ishii, Daisuke, Yonezaki, Naoki, Goldsztejn, Alexandre
#FOS: Computer and information sciences #FOS: Electrical engineering #FOS: Mathematics #Logic in Computer Science (cs.LO) #Numerical Analysis (math.NA) #Systems and Control (eess.SY) #electronic engineering #information engineering
paper · doi:10.48550/arxiv.1506.01762
Verification of temporal logic properties plays a crucial role in proving the desired behaviors of hybrid systems. In this paper, we propose an interval method for verifying the properties described by a bounded linear temporal logic. We relax the problem to allow outputting an inconclusive result when verification process cannot succeed with a prescribed precision, and present an efficient and rigorous monitoring algorithm that demonstrates that the problem is decidable. This algorithm performs a forward simulation of a hybrid automaton, detects a set of time intervals in which the atomic propositions hold, and validates the property by propagating the time intervals. A continuous state at a certain time computed in each step is enclosed by an interval vector that is proven to contain a unique solution. In the experiments, we show that the proposed method provides a useful tool for formal analysis of nonlinear and complex hybrid systems.