Sciweavers

Share
LATA
2016
Springer

A Logical Characterization for Dense-Time Visibly Pushdown Automata

3 years 13 days ago
A Logical Characterization for Dense-Time Visibly Pushdown Automata
Two of the most celebrated results that effectively exploit visual representation to give logical characterization and decidable modelchecking include visibly pushdown automata (VPA) by Alur and Madhusudan and event-clock automata (ECA) by Alur, Fix and Henzinger. VPA and ECA—by making the call-return edges visible and by making the clock-reset operation visible, respectively—recover decidability for the verification problem for pushdown automata implementation against visibly pushdown automata specification and timed automata implementation against event-clock timed automata specification, respectively. In this work we combine and extend these two works to introduce dense-time visibly pushdown automata that make both the call-return as well as resets visible. We present MSO logic characterization of these automata and prove the decidability of the emptiness problem for these automata paving way for verification problem for dense-timed pushdown automata against dense-timed vis...
Devendra Bhave, Vrunda Dave, Shankara Narayanan Kr
Added 07 Apr 2016
Updated 07 Apr 2016
Type Journal
Year 2016
Where LATA
Authors Devendra Bhave, Vrunda Dave, Shankara Narayanan Krishna, Ramchandra Phawade, Ashutosh Trivedi
Comments (0)
books