Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains
Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains
复制标题
线性不等式 LTL (iLTL)：离散时间马尔可夫链的模型检查器
DOI：
10.1007/978-3-540-30482-1_21
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
G. Agha
中科院分区：
文献类型：
--
作者：
YoungMin Kwon;G. Agha
我们开发了一种分析使用离散时间马尔可夫链（DTMC）建模的系统的行为的方法。具体来说，我们定义iLTL，线性不等式的pmf向量作为原子命题的LTL。iLTL允许我们表达不仅属性，如预期的工作数量或预期的能源消耗的协议在一个时间间隔内，但这些值的不平等。我们提出了一种用于iLTL中表达的DTMC的模型检查属性的算法。我们的模型检查器不同于现有的概率，因为后者不检查概率质量函数（pmf）本身的过渡属性。因此，在给定当前pmf的区间估计值的情况下，iLTLtdem可以检查未来的pmf是否总是满足规范。我们相信，这样的属性经常出现在分布式系统和网络中，可能，特别是，在指定路由或负载平衡协议的要求是有用的。我们的算法已经实现了一个工具，称为iLTLtd.，我们说明了使用的工具，通过一些例子。
We develop a way of analyzing the behavior of systems modeled using Discrete Time Markov Chains (DTMC). Specifically, we define iLTL, an LTL with linear inequalities on the pmf vectors as atomic propositions. iLTL allows us to express not only properties such as the expected number of jobs or the expected energy consumption of a protocol during a time interval, but also inequalities over such values. We present an algorithm for model checking properties of DTMCs expressed in iLTL. Our model checker differs from existing probabilistic ones in that the latter do not check properties of the transitions on the probability mass function (pmf) itself. Thus, iLTLChecker can check, given an interval estimate of current pmf, whether future pmfs will always satisfy a specification. We believe such properties often arise in distributed systems and networks and may, in particular, be useful in specifying requirements for routing or load balancing protocols. Our algorithm has been implemented in a tool called iLTLChecker and we illustrate the use of the tool by means of some examples.