A Decidable Probability Logic for Timed Probabilistic Systems
计算机科学中的逻辑
2007-05-23 v2
摘要
In this paper we extend the predicate logic introduced in [Beauquier et al. 2002] in order to deal with Semi-Markov Processes. We prove that with respect to qualitative probabilistic properties, model checking is decidable for this logic applied to Semi-Markov Processes. Furthermore we apply our logic to Probabilistic Timed Automata considering classical and urgent semantics, and considering also predicates on clock. We prove that results on Semi Markov Processes hold also for Probabilistic Timed Automata for both the two semantics considered. Moreover, we prove that results for Markov Processes shown in [Beauquier et al. 2002] are extensible to Probabilistic Timed Automata where urgent semantics is considered.
引用
@article{arxiv.cs/0411100,
title = {A Decidable Probability Logic for Timed Probabilistic Systems},
author = {Ruggero Lanotte and Daniele Beauquier},
journal= {arXiv preprint arXiv:cs/0411100},
year = {2007}
}