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 条

[1] Model-checking Timed Temporal Logics
Bouyer, Patricia
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 231 : 323 - 341
[2] Model-checking the Preservation of Temporal Properties upon Feature Integration
Guelev, Dimitar P.
Ryan, Mark
Schobbens, Pierre Yves
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 128 (06) : 311 - 324
[3] Model-checking the preservation of temporal properties upon feature integration
Guelev D.P.
Ryan M.D.
Schobbens P.Y.
[J]. International Journal on Software Tools for Technology Transfer, 2007, 9 (1) : 53 - 62
[4] Model-checking temporal behaviour in CSP
Ouaknine, J
Reed, GM
[J]. INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS I-V, PROCEEDINGS, 1999, : 295 - 304
[5] Model-Checking Temporal Properties of Real-Time HTL Programs
Carvalho, Andre
Carvalho, Joel
Pinto, Jorge Sousa
de Sousa, Simao Melo
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 191 - +
[6] From Model-Checking to Temporal Logic Constraint Solving
Fages, Francois
Rizk, Aurelien
[J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING, 2009, 5732 : 319 - 334
[7] On the Decidability of Model-Checking Information Flow Properties
D'Souza, Deepak
Holla, Raveendra
Kulkarni, Janardhan
Ramesh, Raghavendra K.
Sprick, Barbara
[J]. INFORMATION SYSTEMS SECURITY, PROCEEDINGS, 2008, 5352 : 26 - +
[8] Model-checking data-aware temporal workflow properties with CTL-FO+
Halle, Sylvain
Villemaire, Roger
Cherkaoui, Omar
Ghandour, Boubker
[J]. 11TH IEEE INTERNATIONAL ENTERPRISE DISTRIBUTED OBJECT COMPUTING CONFERENCE, PROCEEDINGS, 2007, : 267 - 278
[9] The model-checking kit
Schröter, C
Schwoon, S
Esparza, J
[J]. APPLICATIONS AND THEORY OF PETRI NETS 2003, PROCEEDINGS, 2003, 2679 : 463 - 472
[10] QLTL Model-Checking
Laroussinie, Francois
Leclercq, Loriane
Sangnier, Arnaud
[J]. 32ND EACSL ANNUAL CONFERENCE ON COMPUTER SCIENCE LOGIC, CSL 2024, 2024, 288

← 1 2 3 4 5 →