Probabilistic Metric Temporal Graph Logic

TL;DR

This paper introduces Probabilistic Metric Temporal Graph Logic (PMTGL), extending existing logics to analyze probabilistic timed behaviors in cyber-physical systems modeled by Probabilistic Timed Graph Transformation Systems, and proposes a bounded model checking approach.

Contribution

It extends Metric Temporal Graph Logic to include probabilistic properties, adapts satisfaction checking for PTGTSs, and combines model checking techniques for probabilistic timed graph analysis.

Findings

Developed PMTGL for probabilistic timed properties

Implemented Bounded Model Checking approach in AutoGraph

Applied approach successfully to a case study

Abstract

Cyber-physical systems often encompass complex concurrent behavior with timing constraints and probabilistic failures on demand. The analysis whether such systems with probabilistic timed behavior ad-here to a given specification is essential. When the states of the system can be represented by graphs, the rule-based formalism of Probabilistic Timed Graph Transformation Systems (PTGTSs) can be used to suitably capture structure dynamics as well as probabilistic and timed behavior of the system. The model checking support for PTGTSs w.r.t. properties specified using Probabilistic Timed Computation Tree Logic (PTCTL) has been already presented. Moreover, for timed graph-based runtime monitoring, Metric Temporal Graph Logic (MTGL) has been developed for stating metric temporal properties on identified subgraphs and their structural changes over time. In this paper, we (a) extend MTGL to the Probabilistic Metric Temporal Graph Logic (PMTGL) by allowing for the specification of probabilistic properties, (b) adapt our MTGL satisfaction checking approach to PTGTSs, and (c) combine the approaches for PTCTL model checking and MTGL satisfaction checking to obtain a Bounded Model Checking (BMC) approach for PMTGL. In our evaluation, we apply an implementation of our BMC approach in AutoGraph to a running example.