Model-Checking of Linear-Time Properties Based on Possibility Measure

TL;DR

This paper develops a method for model-checking linear-time properties in possibilistic Kripke structures using possibility measures, extending traditional techniques to handle uncertainty in system verification.

Contribution

It introduces possibilistic Kripke structures and possibility measures, and transforms the verification of regular safety and -regular properties into reachability problems within these structures.

Findings

Verification of regular safety and -regular properties can be reduced to reachability checks.

Finite automata can be used to verify regular properties in possibilistic structures.

Examples demonstrate the applicability of the proposed methods.

Abstract

We study the LTL model-checking in possibilistic Kripke structure using possibility measure. First, the notion of possibilistic Kripke structure and the related possibility measure are introduced, then model-checking of reachability and repeated reachability linear-time properties in finite possibilistic Kripke structure are studied. Standard safety property and -regular property in possibilistic Kripke structure are introduced, the verification of regular safety property and -regular property using finite automata are thoroughly studied. It has been shown that the verification of regular safety property and -regular property in finite possibilistic Kripke structure can be transformed into the verification of reachability property and repeated reachability property in the product possibilistic Kripke structure introduced in this paper. Several examples are given to illustrate the methods presented in the paper.