Quantitative Computation Tree Logic Model Checking Based on Generalized Possibility Measures

TL;DR

This paper extends possibilistic computation tree logic model checking using generalized possibility and necessity measures, providing algorithms and complexity analysis, demonstrated through a thermostat example.

Contribution

It introduces GPoCTL based on generalized measures, extending prior possibilistic logic model checking with new algorithms and complexity insights.

Findings

Developed GPoCTL model checking method.

Compared GPoCTL with PoCTL from 2013.

Illustrated method with a thermostat example.

Abstract

We study generalized possibilistic computation tree logic model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Y.Li, Y.Li and Z.Ma (2014). The system is modeled by generalized possibilistic Kripke structures (GPKS, in short), and the verifying property is specified by a generalized possibilistic computation tree logic (GPoCTL, in short) formula. Based on generalized possibility measures and generalized necessity measures, the method of generalized possibilistic computation tree logic model checking is discussed, and the corresponding algorithm and its complexity are shown in detail. Furthermore, the comparison between PoCTL introduced in (2013) and GPoCTL is given. Finally, a thermostat example is given to illustrate the GPoCTL model-checking method.