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.


翻译:网络物理系统通常包含复杂的同时行为,同时有时间限制和需求时的概率性失常。分析是否具有根据特定规格进行概率定时行为分析至关重要。当系统状态可以用图表代表时,可以使用概率定时图表转换系统(PTGTS)的基于规则的形式主义来适当捕捉结构动态以及系统的概率性和定时行为。对使用概率定时计算树逻辑(PTCTL)指定的属性的模型检查支持已经提出。此外,对于基于时间定时的图表运行时间监测而言,已开发出基于规则的系统状态,用以说明所查明的子图的参数及其随着时间的推移的结构性变化。在本文中,我们(a)将MTGLL扩大到概率定时性图(PMTGL),允许对稳定性定时性能进行规范,(b)调整我们的BMTGMTL逻辑模型的满意度检查方法,并(BGGMTMT) 将我们的运行性测试方法应用到我们BGMTMT的满意度模型。

0
下载
关闭预览

相关内容

专知会员服务
28+阅读 · 2021年8月2日
【图与几何深度学习】Graph and geometric deep learning,49页ppt
因果图,Causal Graphs,52页ppt
专知会员服务
246+阅读 · 2020年4月19日
图神经网络库PyTorch geometric
图与推荐
17+阅读 · 2020年3月22日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
已删除
雪球
6+阅读 · 2018年8月19日
Arxiv
0+阅读 · 2021年8月17日
Arxiv
7+阅读 · 2019年6月20日
Logically-Constrained Reinforcement Learning
Arxiv
3+阅读 · 2018年12月6日
Arxiv
4+阅读 · 2018年1月15日
VIP会员
相关资讯
图神经网络库PyTorch geometric
图与推荐
17+阅读 · 2020年3月22日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
meta learning 17年:MAML SNAIL
CreateAMind
11+阅读 · 2019年1月2日
disentangled-representation-papers
CreateAMind
26+阅读 · 2018年9月12日
已删除
雪球
6+阅读 · 2018年8月19日
相关论文
Top
微信扫码咨询专知VIP会员