Quantitative model checking of linear-time properties based on generalized possibility measures

DOI10.1016/J.FSS.2017.03.012MaRDI QIDQ1697514zbMATH OpenOpenAlexFDO

Authors Yongming Li

Publication date 20 February 2018

Published in Fuzzy Sets and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1601.06504

zbMATH Keywords

model checkinglinear temporal logicpossibility theoryfuzzy finite automatonfuzzy regular languagegeneralized possibilistic Kripke structure

Mathematics Subject Classification ID

Reasoning under uncertainty in the context of artificial intelligence (68T37) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Abstract: Model checking of linear-time properties based on possibility measures was studied in previous work (Y. Li and L. Li, Model checking of linear-time properties based on possibility measure, IEEE Transactions on Fuzzy Systems, 21(5)(2013), 842-854). However, the linear-time properties considered in the previous work was classical and qualitative, possibility information of the systems was not considered at all. We shall study quantitative model checking of fuzzy linear-time properties based on generalized possibility measures in the paper. Both the model of the system, as well as the properties the system needs to adhere to, are described using possibility information to identify the uncertainty in the model/properties. The systems are modeled by {sl generalized possibilistic Kripke structures} (GPKS, in short), and the properties are described by fuzzy linear-time properties. Concretely, fuzzy linear-time properties about reachability, always reachability, constrain reachability, repeated reachability and persitence in GPKSs are introduced and studied. Fuzzy regular safety properties and fuzzy $omega-$regular properties in GPKSs are introduced, the verification of fuzzy regular safety properties and fuzzy $omega-$regular properties using fuzzy finite automata are thoroughly studied. It has been shown that the verification of fuzzy regular safety properties and fuzzy $omega-$regular properties in a finite GPKS can be transformed into the verification of (always) reachability properties and repeated reachability (persistence) properties in the product GPKS introduced in this paper. Several examples are given to illustrate the methods presented in the paper.

Recommendations

• Model checking of reachability problems based on generalized possibility measures
• Model checking linear-time properties of probabilistic systems
• Quantitative Model Checking Revisited: Neither Decidable Nor Approximable
• Model checking of linear-time properties in multi-valued systems
• Model checking quantitative hyperproperties
• scientific article; zbMATH DE number 2102708
• scientific article; zbMATH DE number 6454071
• Quantified Linear Temporal Logic over Probabilistic Systems with an Application to Vacuity Checking
• Robust Model-Checking of Linear-Time Properties in Timed Automata

Cites work

• scientific article; zbMATH DE number 1693429 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3212004 (Why is no real title available?)
• A fuzzy real-time temporal logic
• Computation tree logic model checking based on possibility measures
• Data structures for symbolic multi-valued model-checking
• Default reasoning and possibility theory
• Discounting in LTL
• Fuzzy Time in Linear Temporal Logic
• Fuzzy finite automata and fuzzy regular expressions with membership values in lattice-ordered monoids
• Fuzzy measures and integrals. Theory and applications
• Fuzzy regular languages over finite and infinite words
• Fuzzy sets
• Fuzzy sets as a basis for a theory of possibility
• Model checking discounted temporal properties
• Model checking fuzzy computation tree logic
• Possibility theory and statistical reasoning
• Probabilistic propositional temporal logics
• Probabilities, possibilities, and fuzzy sets
• Quantitative \(\mu\)-calculus and CTL defined over constraint semirings

Cited in

(13)

• Computation tree logic model checking based on multi-valued possibility measures
• Model checking quantitative hyperproperties
• Generalized possibility computation tree logic with frequency and its model checking
• Characterization and computation of approximate bisimulations for fuzzy automata
• Model checking of fuzzy linear temporal logic based on quantum logic
• Fuzzy alternating Büchi automata over distributive lattices
• Fuzzy \(\epsilon\)-approximate regular languages and minimal deterministic fuzzy automata \(\epsilon\)-accepting them
• Fuzzy alternating automata over distributive lattices
• Coherent checking and updating of Bayesian models without specifying the model space: a decision-theoretic semantics for possibility theory
• Towards contingent world descriptions in description logics
• Model checking of reachability problems based on generalized possibility measures
• Approximate bisimulations and state reduction of fuzzy automata under fuzzy similarity measures
• Computation tree logic model checking over possibilistic decision processes under finite-memory scheduler

This page was built for publication: Quantitative model checking of linear-time properties based on generalized possibility measures

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1697514)