Analyzing Oscillatory Behavior with Formal Methods

An important behavioral pattern that can be witnessed in many systems is periodic re-occurrence. For example, most living organisms that we know are governed by a 24 hours rhythm that determines whether they are awake or not. On a larger scale, also whole population numbers of organisms fluctuate in a cyclic manner as in predator-prey relationships. When treating such systems in a deterministic way, i.e., assuming that stochastic effects are negligible, the analysis is a well-studied topic. But if those effects play an important role, recent publications suggest that at least a part of the system should be modeled stochastically. However, in that case, one quickly realizes that characterizing and defining oscillatory behavior is not a straightforward task, which can be solved once and for all. Moreover, efficiently checking whether a given system oscillates or not and if so determining the amplitude of the fluctuations and the time in-between is intricate. This paper shall give an overview of the existing literature on different modeling formalisms for oscillatory systems, definitions of oscillatory behavior, and the respective analysis methods.