Tableau-based automata construction for dynamic linear time temporal logic

被引：10

作者：

Giordano, Laura ^{[1
]}

Martelli, Alberto

机构：

[1] Univ Piemonte Orientale, Dipartimento Informat, Alessandria, Italy

[2] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy

来源：

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE | 2006年 / 46卷 / 03期

关键词：

temporal logic; model checking;

D O I：

10.1007/s10472-006-9020-7

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

We present a tableau-based algorithm for obtaining a Buchi automaton from a formula in Dynamic Linear Time Temporal Logic (DLTL), a logic which extends LTL by indexing the until operator with regular programs. The construction of the states of the automaton is similar to the standard construction for LTL, but a different technique must be used to verify the fulfillment of until formulas. The resulting automaton is a Buchi automaton rather than a generalized one. The construction can be done on-the-fly, while checking for the emptiness of the automaton. We also extend the construction to the Product Version of DLTL.

引用

页码：289 / 315

页数：27

共 24 条

[1]

[Anonymous], 1991, Artificial intelligence and mathematical theory of computation: papers in honor of John McCarthy, DOI DOI 10.1016/B978-0-12-450010-5.50026-8

[2] Planning for temporally extended goals [J].

Bacchus, F ;

Kabanza, F .

ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 1998, 22 (1-2) :5-27

[3]

Calvanese D., 2002, Principles of Knowledge Representation and Reasoning, P593

[4]

Daniele M., 1999, Computer Aided Verification. 11th International Conference, CAV'99. Proceedings (Lecture Notes in Computer Science Vol.1633), P249

[5]

Gerth R., 1996, Protocol Specification, Testing and Verification XV. Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, P3

[6] Verifying communicating agents by model checking in a temporal action logic [J].

Giordano, L ;

Martelli, A ;

Schwind, C .

LOGICS IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2004, 3229 :57-69

[7]

Giordano L, 2003, LECT NOTES ARTIF INT, V2829, P262

[8]

Giordano L., 2001, LOG J IGPL, V9, P289

[9]

Giunchiglia F, 2000, LECT NOTES ARTIF INT, V1809, P1

[10] Dynamic linear time temporal logic [J].

Henriksen, JG ;

Thiagarajan, PS .

ANNALS OF PURE AND APPLIED LOGIC, 1999, 96 (1-3) :187-207

← 1 2 3 →