概率度量时态图逻辑
Probabilistic Metric Temporal Graph Logic
摘要：
网络物理系统通常包含复杂的并发行为，具有时序约束和按需故障的概率。分析这类具有概率定时行为的系统是否符合给定的规范是必不可少的。当系统的状态可以用图表示时，概率时间图变换系统（PTGTS）的基于规则的形式主义可以用来适当地捕获结构动力学以及系统的概率和时间行为。PTGTS的模型检验支持w.r.t.使用概率计时计算树逻辑（PTCTL）指定的属性已经呈现。此外，对于基于定时图的运行时监控，度量时态图逻辑（MTGL）已经被开发用于在所识别的子图上陈述度量时态属性及其随时间的结构变化。在本文中，我们（a）扩展MTGL的概率度量时态图逻辑（PMTGL）的概率属性的规格，（b）适应我们的MTGL满意度检查方法PTGTS，和（c）结合PTCTL模型检验和MTGL满意度检查的方法，以获得一个有界模型检验（BMC）的PMTGL方法。在我们的评估中，我们将我们的BMC方法在AutoGraph中的实现应用于一个运行的示例。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
