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

共 50 条

[41] Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results
Bultan, T
Gerber, R
Pugh, W
[J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1999, 21 (04): : 747 - 789
[42] Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results
University of Maryland, College Park, MD, United States
不详
不详
[J]. ACM Trans Program Lang Syst, 4 (747-789):
[43] Connectivity testing through model-checking
Godskesen, JC
Nielsen, B
Skou, A
[J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2004, PROCEEDINGS, 2004, 3235 : 167 - 184
[44] Foundations of incremental aspect model-checking
Krishnamurthi, Shriram
Fisler, Kathi
[J]. ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY, 2007, 16 (02)
[45] Model-checking access control policies
Guelev, DP
Ryan, M
Schobbens, PY
[J]. INFORMATION SECURITY, PROCEEDINGS, 2004, 3225 : 219 - 230
[46] Model-checking TRIO specifications in SPIN
Morzenti, A
Pradella, M
San Pietro, P
Spoletini, P
[J]. FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 542 - 561
[47] A Model-Checking Tool for Families of Services
Asirelli, Patrizia
ter Beek, Maurice H.
Fantechi, Alessandro
Gnesi, Stefania
[J]. FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, 2011, 6722 : 44 - 58
[48] On complexity of model-checking for the TQL logic
Boneva, I
Talbot, JM
[J]. EXPLORING NEW FRONTIERS OF THEORETICAL INFORMATICS, 2004, 155 : 381 - 394
[49] Model-checking trace event structures
Madhusudan, P
[J]. 18TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2003, : 371 - 380
[50] Systematic construction of abstractions for model-checking
Gurfinkel, A
Wei, O
Chechik, M
[J]. VERIFICATION, MODEL CHECKING , AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2006, 3855 : 381 - 397

← 1 2 3 4 5 →