Voir la notice de l'article provenant de la source Numdam
A standard bridge between automata theory and logic is provided by the notion of characteristic formula. This paper investigates this problem for the class of event-recording automata (ERA), a subclass of timed automata in which clocks are associated with actions and that enjoys very good closure properties. We first study the problem of expressing characteristic formulae for ERA in Event-Recording Logic (ERL ), a logic introduced by Sorea to express event-based timed specifications. We prove that the construction proposed by Sorea for ERA without invariants is incorrect. More generally, we prove that timed bisimilarity cannot in general be expressed in ERL for the class of ERA , and study under which conditions on ERA it can be. Then, we introduce the logic WTμ , a new logic for event-based timed specifications closer to the timed logic ℒν that was introduced by Laroussinie, Larsen and Weise. We prove that it is strictly more expressive than ERL , and that its model-checking problem against ERA is EXPTIME -complete. Finally, we provide characteristic formulae constructions in WTμ for characterizing the general class of ERA up to timed (bi)similarity and study the complexity issues.
@article{ITA_2013__47_1_69_0,
author = {Nguena Timo, Omer Landry and Reynier, Pierre-Alain},
title = {On characteristic formulae for {Event-Recording} {Automata}},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
pages = {69--96},
publisher = {EDP-Sciences},
volume = {47},
number = {1},
year = {2013},
doi = {10.1051/ita/2012029},
mrnumber = {3072311},
language = {en},
url = {http://geodesic.mathdoc.fr/articles/10.1051/ita/2012029/}
}
TY - JOUR AU - Nguena Timo, Omer Landry AU - Reynier, Pierre-Alain TI - On characteristic formulae for Event-Recording Automata JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2013 SP - 69 EP - 96 VL - 47 IS - 1 PB - EDP-Sciences UR - http://geodesic.mathdoc.fr/articles/10.1051/ita/2012029/ DO - 10.1051/ita/2012029 LA - en ID - ITA_2013__47_1_69_0 ER -
%0 Journal Article %A Nguena Timo, Omer Landry %A Reynier, Pierre-Alain %T On characteristic formulae for Event-Recording Automata %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2013 %P 69-96 %V 47 %N 1 %I EDP-Sciences %U http://geodesic.mathdoc.fr/articles/10.1051/ita/2012029/ %R 10.1051/ita/2012029 %G en %F ITA_2013__47_1_69_0
Nguena Timo, Omer Landry; Reynier, Pierre-Alain. On characteristic formulae for Event-Recording Automata. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 1, pp. 69-96. doi: 10.1051/ita/2012029
Cité par Sources :