Name
Abstract | ||
|---|---|---|
We present a new algorithm formodel-checkingweakmonadic second-order logic on inductive structures, a class of structures of bounded clique width. Our algorithm directly manipulates formulas and checks them on the structure of interest, thus avoiding both the use of automata and the need to interpret the structure in the binary tree. In addition to the algorithm, we give a new proof of decidability of weak MSO on inductive structures which follows Shelah's composition method. Generalizing this proof technique, we obtain decidability of weak MSO extended with the unbounding quantifier on the binary tree, which was open before. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1007/978-3-642-15205-4_29 | CSL |
Keywords | Field | DocType |
proof technique,inductive structure,binary tree,unbounding quantifier,bounded clique width,weak monadic second-order logic,new proof,weak mso,composition method,new algorithm formodel-checkingweakmonadic second-order,model checking | Discrete mathematics,Combinatorics,Generalization,Automaton,Algorithm,Monadic second-order logic,Binary tree,Decidability,Clique-width,Mathematics,Bounded function | Conference |
Volume | ISSN | ISBN |
6247 | 0302-9743 | 3-642-15204-X |
Citations | PageRank | References |
4 | 0.47 | 7 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Tobias Ganzow | 1 | 40 | 2.26 |
| Łukasz Kaiser | 2 | 2307 | 89.08 |