Kripke structures are important modeling formalisms to understand the behavior of reactive systems. We present an approach to automatically infer Kripke structures from time series datasets. Our algorithm bridges the continuous world of time profiles and the discrete symbols of Kripke structures by incorporating a segmentation algorithm as an intermediate step. This approach identifies, in an unsupervised manner, the states of the Kripke structure, the transition relation, and the properties (propositions) that hold true in each state. We demonstrate experimental results of our approach to understanding the interplay between key biological processes.