  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.
