Optimistic and Pessimistic On-the-fly Analysis for Metric Temporal Graph Logic

Abstract

The nonpropositional Metric Temporal Graph Logic (MTGL) specifies the behavior of timed dynamic systems given by timed graph sequences (TGSs), which contain typed attributed graphs representing system states and the elapsed time between states. MTGL satisfaction can be analyzed for finite TGSs by translating its satisfaction problem to the satisfaction problem of nested graph conditions using a folding operation (aggregating a TGS into a graph with history) and a reduction operation (translating an MTGL condition into a nested graph condition). In this paper, we introduce an analysis procedure for MTGL to allow for an on-the-fly analysis of finite/infinite TGSs. To this end, we introduce a further (optimistic) reduction of MTGL conditions, which leads to violations during the on-the-fly analysis only when non-satisfaction is guaranteed in the future whereas the former (pessimistic) reduction leads to violations when satisfaction is not guaranteed in the future. We motivate the relevance of our analysis procedure, which uses both reduction operations, by means of a running example. Finally, we discuss prototypical support in the tool AutoGraph.