On Clock-Aware LTL Properties of Timed Automata

被引：0

作者：

Bezdek, Peter ^{[1
]}

Benes, Nikola ^{[1
]}

Havel, Vojtech ^{[1
]}

Barnat, Jiri ^{[1
]}

Cerna, Ivana ^{[1
]}

机构：

[1] Masaryk Univ, Fac Informat, Brno, Czech Republic

来源：

THEORETICAL ASPECTS OF COMPUTING - ICTAC 2014 | 2014年 / 8687卷

关键词：

Linear Temporal Logic; Timed Automata; Automata-based Model Checking; CHECKING; SYSTEMS;

D O I：

暂无

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We introduce the Clock-Aware Linear Temporal Logic (CALTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed B " uchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.

引用

页码：43 / 60

页数：18

共 50 条

[1] On clock-aware LTL properties of timed automata
Bezděk, Peter
Beneš, Nikola
Havel, Vojtěch
Barnat, Jiří
Černá, Ivana
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2014, 8687 : 43 - 60
[2] On clock-aware LTL parameter synthesis of timed automata
Bezdek, Peter
Benes, Nikola
Cerna, Ivana
Barnat, Jiri
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2018, 99 : 114 - 142
[3] Timed automata and additive clock constraints
Bérard, B
Dufourd, C
INFORMATION PROCESSING LETTERS, 2000, 75 (1-2) : 1 - 7
[4] Probabilistic Timed Automata with Clock-Dependent Probabilities
Sproston, Jeremy
FUNDAMENTA INFORMATICAE, 2021, 178 (1-2) : 101 - 138
[5] PROBABILISTIC TIMED AUTOMATA WITH ONE CLOCK AND INITIALISED CLOCK-DEPENDENT PROBABILITIES
Sproston, Jeremy
LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (04) : 6:1 - 6:35
[6] Event-clock automata: a determinizable class of timed automata
Alur, R
Fix, L
Henzinger, TA
THEORETICAL COMPUTER SCIENCE, 1999, 211 (1-2) : 253 - 273
[7] Clock Allocation in Timed Automata and Graph Colouring
Saeedloei, Neda
Kluzniak, Feliks
HSCC 2018: PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL (PART OF CPS WEEK), 2018, : 71 - 80
[8] Dynamical properties of timed automata
Puri, A
DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2000, 10 (1-2): : 87 - 113
[9] Dynamical properties of timed automata
Puri, A
FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 210 - 227
[10] Dynamical Properties of Timed Automata
Anuj Puri
Discrete Event Dynamic Systems, 2000, 10 : 87 - 113

← 1 2 3 4 5 →