The Complexity of Dual Models Problem of Propositional Linear Temporal Logics
DOI:
Author:
Affiliation:

Clc Number:

Fund Project:

  • Article
  • |
  • Figures
  • |
  • Metrics
  • |
  • Reference
  • |
  • Related
  • |
  • Cited by
  • |
  • Materials
  • |
  • Comments
    Abstract:

    In this paper, the concept of dual models of a propositional linear temporal logic formula is defined: A formula f has dual models if it has two models (namely two w-sequences of states) such that the assignments to atomic propositions at each position of them are dual. Then for various propositional linear temporal logics, the complexity of the problem deciding whether a formula f has dual models (denoted by DM) and the problem of determination of dual models in a Kripke-structure for a formula f (denoted by KDM) are investigated. It is shown that DM and KDM are NP-complete for the logic with F("Future") operator, and they are PSPACE-complete for the logic with F,X("Next") operators, the logic with U("Until") operator, the logic with U, S, X operators, and the logic with regular operators given by Wolper (known as extended temporal logic, ETL).

    Reference
    Related
    Cited by
Get Citation

吴志林,张文辉.命题线性时序逻辑的对偶模型问题的复杂性.软件学报,2007,18(7):1573-1581

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:July 08,2005
  • Revised:February 23,2006
  • Adopted:
  • Online:
  • Published:
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address:4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code:100190
Phone:010-62562563 Fax:010-62562533 Email:jos@iscas.ac.cn
Technical Support:Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063