Combining Paraconsistency and Probability in CTL

Norihiro Kamide, Daiki Koizumi

2015

Abstract

Computation tree logic (CTL) is known to be one of the most useful temporal logics for verifying concurrent systems by model checking technologies. However, CTL is not sufficient for handling inconsistency-tolerant and probabilistic accounts of concurrent systems. In this paper, a paraconsistent (or inconsistency-tolerant) probabilistic computation tree logic (PpCTL) is derived from an existing probabilistic computation tree logic (pCTL) by adding a paraconsistent negation connective. A theorem for embedding PpCTL into pCTL is proven, which indicates that we can reuse existing pCTL-based model checking algorithms. Some illustrative examples involving the use of PpCTL are also presented.

Paper Citation

in Harvard Style

Kamide N. and Koizumi D. (2015). Combining Paraconsistency and Probability in CTL . In Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART, ISBN 978-989-758-074-1, pages 285-293. DOI: 10.5220/0005180402850293

in Bibtex Style

@conference{icaart15,
author={Norihiro Kamide and Daiki Koizumi},
title={Combining Paraconsistency and Probability in CTL},
booktitle={Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART,},
year={2015},
pages={285-293},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005180402850293},
isbn={978-989-758-074-1},
}

in EndNote Style

TY - CONF
JO - Proceedings of the International Conference on Agents and Artificial Intelligence - Volume 2: ICAART,
TI - Combining Paraconsistency and Probability in CTL
SN - 978-989-758-074-1
AU - Kamide N.
AU - Koizumi D.
PY - 2015
SP - 285
EP - 293
DO - 10.5220/0005180402850293