Expressiveness of propositional projection temporal logic with star

被引：33

作者：

Tian, Cong ^{[1
]}

Duan, Zhenhua ^{[1
]}

机构：

[1] Xidian Univ, ICTT & ISN Lab, Xian 710071, Peoples R China

来源：

THEORETICAL COMPUTER SCIENCE | 2011年 / 412卷 / 18期

关键词：

Temporal logic; Expressiveness; Automata theory; Regular expressions; Verification;

D O I：

10.1016/j.tcs.2010.12.047

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper investigates the expressiveness of Propositional Projection Temporal Logic with Star (PPTL*). To this end, Buchi automata and omega-regular expressions are first extended as Stutter Buchi Automata (SBA) and Extended Regular Expressions (ERE) to include both finite and infinite strings. Further, by equivalent transformations among PPTL* formulas, SBAs and EREs. PPTL* is proved to represent exactly the full regular language. Moreover, some fragments of PPTL* are characterized, and finally, PPTL* and its fragments are classified into five different language classes. (C) 2010 Elsevier B.V. All rights reserved.

引用

页码：1729 / 1744

页数：16

共 28 条

[1]

[Anonymous], P 15 ACM S PRINC PRO

[2]

[Anonymous], 1984, PROC 16 ACM S THEORY, DOI DOI 10.1145/800057.808665

[3]

[Anonymous], THEORY COMPUTING MAC

[4]

[Anonymous], 1983, Ph.D. thesis

[5]

[Anonymous], 1 ANN IEEE S LOG COM

[6]

BARRINGER H, 1985, P IFIP C ROL ABSTR M

[7]

Duan ZH., 1996, THESIS U NEWCASTLE T

[8] A decision procedure for propositional projection temporal logic with infinite models [J].

Duan, Zhenhua ;

Tian, Cong ;

Zhang, Li .

ACTA INFORMATICA, 2008, 45 (01) :43-78

[9] Framed temporal logic programming [J].

Duana, Zhenhua ;

Yanga, Xiaoxiao ;

Koutnyb, Maciej .

SCIENCE OF COMPUTER PROGRAMMING, 2008, 70 (01) :31-61

[10]

EMERSON E, 1990, HDB THEORETICAL COMP, pCH16

← 1 2 3 →