Name
Abstract | ||
|---|---|---|
We study linear time model checking of collapsible higher-order pushdown systems (CPDS) of order 2 (manipulating stack of stacks) against MSO and PDL (propositional dynamic logic with converse and loop) enhanced with push/pop matching relations. To capture these linear time behaviours with matchings, we propose order-2 nested words. These graphs consist of a word structure augmented with two binary matching relations, one for each order of stack, which relate a push with matching pops (or collapse) on the respective stack. Due to the matching relations, satisfiability and model checking are undecidable. Hence we propose an under-approximation, bounding the number of times an order-1 push can be popped. With this under-approximation, which still allows unbounded stack height, we get decidability for satisfiability and model checking of both MSO and PDL. The problems are ExpTime-Complete for PDL. |
Year | Venue | Field |
|---|---|---|
2016 | arXiv: Formal Languages and Automata Theory | Discrete mathematics,Combinatorics,Model checking,Nested word,Nested stack automaton,Satisfiability,Decidability,Dynamic logic (digital electronics),Time complexity,Mathematics,Undecidable problem |
DocType | Volume | Citations |
Journal | abs/1609.06290 | 1 |
PageRank | References | Authors |
0.36 | 1 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Cyriac Aiswarya | 1 | 3 | 1.06 |
| Paul Gastin | 2 | 1165 | 75.66 |
| Prakash Saivasan | 3 | 34 | 7.49 |