论文标题
概率系统的上下文感知的时间逻辑
Context-Aware Temporal Logic for Probabilistic Systems
论文作者
论文摘要
在本文中，我们介绍了上下文感知的概率时间逻辑（CAPTL），该概率是通过一组具有基于上下文的优先级结构的PCTL目标来形式化系统要求的直观方式。我们正式介绍了Captl的语法和语义，并提出了用于CAPTL要求的合成算法。我们还基于Prism-Games模型检查器实现算法。最后，我们在两个案例研究中证明了Captl的用法：机器人任务计划问题，并合成微电极 - 电极 - 阵列数字微流体生物芯片的错误弹性调度程序。
In this paper, we introduce the context-aware probabilistic temporal logic (CAPTL) that provides an intuitive way to formalize system requirements by a set of PCTL objectives with a context-based priority structure. We formally present the syntax and semantics of CAPTL and propose a synthesis algorithm for CAPTL requirements. We also implement the algorithm based on the PRISM-games model checker. Finally, we demonstrate the usage of CAPTL on two case studies: a robotic task planning problem, and synthesizing error-resilient scheduler for micro-electrode-dot-array digital microfluidic biochips.
