首页|An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking

An Automata-Theoretic Approach to L-valued Computation Tree Logic Model Checking

扫码查看
原文链接
  • NETL
  • NSTL
  • 万方数据
  • 维普
Translating computation tree logic formu-las into Büchi tree automata has been proven to be an effective approach for implementing branching-time model checking. For a more generalized class of lattice-valued (L-valued, for short) computation tree logic formulas, the revelent study has not proceeded yet. We introduce the notion of L-valued alternating Büchi tree automata and achieve the goal of associating each L-valued computation tree logic formula with an L-valued Büchi tree automaton. We show that a satisfiability problem for an L-valued computation tree logic formula can be reduced to one for the language accepted by an L-valued Büchi tree automaton. L-valued alternating Büchi tree automata are the key to the automata-theoretic approach to L-valued computation tree logics, and we also study their expressive power and closure properties.

L-valued computation tree logicsL-valued alternating Büchi tree automataL-valued positive Boolean formulasDual operation

WEI Xiujuan、LI Yongming

展开 >

College of Mathematic and Information Science, Shaanxi Normal University, Xi'an 710119, China

College of Computer Science, Shaanxi Normal University, Xi'an 710119, China

This work is supported by the National Natural Science Foundation of ChinaThis work is supported by the National Natural Science Foundation of ChinaPh.D.Programs Foundation of Ministry of Education of China

11271237No.1167124420130202110001

2019

10.1049/cje.2019.01.014

中国电子杂志(英文版)

中国电子杂志(英文版)

CSTPCDCSCDSCIEI
ISSN：1022-4653
年,卷(期)：2019.28(2)
  • 1
  • 27