Name
Abstract | ||
|---|---|---|
We consider the model-checking problem for data multi-pushdown automata (DMPA). DMPA generate data words, i.e, strings enriched with values from an infinite domain. The latter can be used to represent an unbounded number of process identifiers so that DMPA are suitable to model concurrent programs with dynamic process creation. To specify properties of data words, we use monadic second-order (MSO) logic, which comes with a predicate to test two word positions for data equality. While satisfiability for MSO logic is undecidable (even for weaker fragments such as first-order logic), our main result states that one can decide if all words generated by a DMPA satisfy a given formula from the full MSO logic. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-28729-9_26 | FoSSaCS |
Keywords | Field | DocType |
concurrent program,dynamic process creation,data word,data multi-pushdown automaton,data equality,infinite domain,full mso logic,first-order logic,model checking language,main result state,mso logic | Discrete mathematics,Model checking,Identifier,Computer science,Automaton,Satisfiability,Predicate (grammar),Transitive closure,Monad (functional programming),Undecidable problem | Conference |
Volume | ISSN | Citations |
7213 | 0302-9743 | 17 |
PageRank | References | Authors |
0.69 | 22 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Benedikt Bollig | 1 | 427 | 35.02 |
| Aiswarya Cyriac | 2 | 58 | 3.31 |
| Paul Gastin | 3 | 1165 | 75.66 |
| K. Narayan Kumar | 4 | 74 | 7.24 |