A Decidable Probability Logic for Timed Probabilistic Systems

Thumbnail Image

Date

Authors

Journal Title

Journal ISSN

Volume Title

Publisher

Abstract

Description

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.

Keywords

Logic in Computer Science, C.3; D.2.4; F.3.1; F.4.1; G.3

Citation

URI

http://salesiana.dossiersoluciones.com/handle/123456789/100621

Consulte el texto completo en el siguiente enlace:

https://arxiv.org/abs/cs/0411100
 http://arxiv.org/abs/cs/0411100

Collections

arXiv