xeLTL: Extending eLTL with variables

Abstract

Our daily activity is increasingly integrated with systems that somehow adapt their behaviour to our state or reactions. These systems are usually called reactive systems since they evolve based on internal or external events produced by their environment. The massive use of smartphones and wearable devices for health monitoring is just an example of how these systems impact in our lives. In addition, some systems, such as those for assisted or autonomous driving, carry out critical tasks. Thus, it is important to ensure that reactive systems satisfy safety requirements in which, in many cases, is relevant the evolution of time or other physical magnitudes. In this paper, we present the eXtended Event-driven Temporal Logic (xeLTL) that can express requirements over intervals of parameterized events.