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