TAGED Approximations for Temporal Properties Model-Checking

被引：0

作者：

Courbis, Romeo ^{[1
]}

Heam, Pierre-Cyrille ^{[1
]}

Kouchnarenko, Olga ^{[1
]}

机构：

[1] Univ Franche Comte, INRIA, CASSIS, LIFC, F-25030 Besancon, France

来源：

IMPLEMENTATION AND APPLICATION OF AUTOMATA, PROCEEDINGS | 2009年 / 5642卷

关键词：

TREE AUTOMATA; LOGIC;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper investigates the use of tree automata with global equalities and disequalities (TAGED for short) in reachability analysis over term rewriting systems (TRSs). The reachability problem being in general undecidable on non terminating TRSs, we provide TAGED-based construction, and then design approximation-based semi-decision procedures to model-check useful temporal patterns on infinite state rewriting graphs. To show that the above TAGED-based construction can be effectively carried out, complexity analysis for rewriting TAGED-definable languages is given.

引用

页码：135 / 144

页数：10

共 31 条

[1]

[Anonymous], 1992, TEMPORAL LOGIC REACT, DOI DOI 10.1007/978-1-4612-0931-7

[2]

[Anonymous], 1998, Term rewriting and all thatM

[3]

ARMANDO A, 2007, CSF, P385

[4] Towards an efficient implementation of tree automata completion [J].

Balland, Emilie ;

Boichut, Yohan ;

Genet, Thomas ;

Moreau, Pierre-Etienne .

ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2008, 5140 :67-+

[5]

BOGAERT B, 1992, LECT NOTES COMPUT SC, V577, P161

[6]

Boichut Y, 2008, LECT NOTES COMPUT SC, V5117, P48, DOI 10.1007/978-3-540-70590-1_4

[7]

BOICHUT Y, 2009, NORDIC J CO IN PRESS

[8]

Boichut Y, 2007, LECT NOTES COMPUT SC, V4533, P48

[9]

Clarke E, 2003, TIME-ICTL 2003: 10TH INTERNATIONAL SYMPOSIUM ON TEMPORAL REPRESENTATION AND REASONING AND FOURTH INTERNATIONAL CONFERENCE ON TEMPORAL LOGIC, PROCEEDINGS, P7

[10]

COMON H, 2005, THEORETICAL COMPUTER, P331

← 1 2 3 4 →