|
Title:
|
TIMED STATE-EVENT AUTOMATA AND ALTERNATION FOR SOFTWARE MODEL CHECKING |
|
Author(s):
|
Abdelaziz Fellah |
|
ISBN:
|
978-972-8924-97-3 |
|
Editors:
|
Hans Weghorn and Pedro Isaías |
|
Year:
|
2009 |
|
Edition:
|
V I, 2 |
|
Keywords:
|
Software model checking, software verification, timed temporal propositional logic, Büchi and alternating automata |
|
Type:
|
Full Paper |
|
First Page:
|
226 |
|
Last Page:
|
233 |
|
Language:
|
English |
|
Cover:
|
|
|
Full Contents:
|
click to dowload 
|
|
Paper Abstract:
|
We present an automata-theoretical framework for the translation of timed state-event linear temporal logic (T e
s LTL)
Formulas into equivalent timed state-event Büchi automata. The relation between timed propositional temporal logic and
automata can be established through languages over infinite words. The approach is enhanced by using alternation, a
powerful parallelism feature to improve and reduce the state-space explosion problem in building large software model
checking systems. |
|
|
|
|
|
|
