具有一个时钟和初始化的时钟相关概率的概率定时自动机
摘要：具有时钟依赖的概率时限自动机通过离散概率选择扩展了经典的时限自动机，其中概率允许依赖于时钟的精确值。先前的工作表明，具有至少三个时钟的时钟依赖概率时限自动机的定量可达性问题是不可判定的。本文考虑了只有一个时钟的时钟依赖概率时限自动机的子类，其时钟依赖由仿射函数描述，并且满足一个初始化条件，要求在采取具有非平凡时钟依赖的边之间的某个时刻，时钟必须具有整数值。我们提出了一种方法，用于在多项式时间内解决这种一时钟初始化的时钟依赖概率时限自动机的定量和定性可达性问题。我们的结果通过转化为区间马尔可夫决策过程获得。
作者：Jeremy Sproston
论文ID：2006.04202
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22