Name
Abstract | ||
|---|---|---|
Two of the most celebrated results that effectively exploit visual representation to give logical characterization and decidable model-checking 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 visibly pushdown automata specification. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-30000-9_7 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
Visibly pushdown,Event-clock,Logical characterization | Deterministic context-free grammar,Discrete mathematics,Embedded pushdown automaton,Nested word,Computer science,Automaton,Deterministic pushdown automaton,Theoretical computer science,Decidability,Pushdown automaton | Conference |
Volume | ISSN | Citations |
9618 | 0302-9743 | 2 |
PageRank | References | Authors |
0.38 | 6 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Devendra Bhave | 1 | 7 | 2.20 |
| Vrunda Dave | 2 | 6 | 2.83 |
| Shankara Narayanan Krishna | 3 | 243 | 42.57 |
| Ramchandra Phawade | 4 | 8 | 2.92 |
| Ashutosh Trivedi | 5 | 149 | 28.08 |