PARTIALLY ORDERED TWO-WAY BUCHI AUTOMATA

被引：2

作者：

Kufleitner, Manfred ^{[1
]}

Lauser, Alexander ^{[1
]}

机构：

[1] Univ Stuttgart, Dept Theoret Comp Sci, D-70569 Stuttgart, Germany

来源：

INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE | 2011年 / 22卷 / 08期

关键词：

Infinite words; two-way Buchi automaton; first-order logic;

D O I：

10.1142/S0129054111009082

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We introduce partially ordered two-way Buchi automata and characterize their expressive power in terms of fragments of first-order logic FO[<]. Partially ordered two-way Buchi automata are Buchi automata which can change the direction in which the input is processed with the constraint that whenever a state is left, it is never re-entered again. Nondeterministic partially ordered two-way Buchi automata coincide with the first-order fragment Sigma(2). Our main contribution is that deterministic partially ordered two-way Buchi automata are expressively complete for the first-order fragment Delta(2). As an intermediate step, we show that deterministic partially ordered two-way Buchi automata are effectively closed under Boolean operations. A small model property yields coNP-completeness of the emptiness problem and the inclusion problem for deterministic partially ordered two-way Buchi automata.

引用

页码：1861 / 1876

页数：16

共 19 条

[1]

Baier C, 2008, PRINCIPLES OF MODEL CHECKING, P1

[2]

Bojanczyk M, 2008, LECT NOTES COMPUT SC, V4962, P172, DOI 10.1007/978-3-540-78499-9_13

[3]

Buchi J. Richard, 1962, P INT C LOG METH PHI, P1, DOI DOI 10.1007/978-1-4613-8928-6_23

[4]

Clarke EM, 1999, MODEL CHECKING, P1

[5]

Dartois L, 2010, LECT NOTES COMPUT SC, V6224, P148, DOI 10.1007/978-3-642-14455-4_15

[6] Alternation Elimination by Complementation (Extended Abstract) [J].

Dax, Christian ;

Klaedtke, Felix .

Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2008, 5330 :214-229

[7] Fragments of First-Order Logic over Infinite Words [J].

Diekert, Volker ;

Kufleitner, Manfred .

THEORY OF COMPUTING SYSTEMS, 2011, 48 (03) :486-516

[8]

Kapoutsis C, 2005, LECT NOTES COMPUT SC, V3618, P544

[9]

Kufleitner M., 2010, LNCS, V6482, P181

[10]

Lodaya K, 2008, INT FED INFO PROC, V273, P461

← 1 2 →