Name
Abstract | ||
|---|---|---|
We use the recently developed theory of forest algebras to find algebraic characterizations of the languages of unranked trees and forests definable in various logics. These include the temporal logics CTL and EF, and first-order logic over the ancestor relation. While the characterizations are in general non-effective, we are able to use them to formulate necessary conditions for definability and provide new proofs that a number of languages are not definable in these logics. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1109/LICS.2009.40 | Logical Methods in Computer Science |
Keywords | DocType | Volume |
tree logics,automatic verification technique,finite-state abstraction,joint paper,forest algebras,graduate students e.a,a.p. sistla,wreath products,model checking,state-transition system,construction industry,wreath product,development theory,algebra,temporal logic,first order logic,data mining,automata | Journal | 8 |
Issue | ISSN | ISBN |
3 | 1043-6871 | 978-0-7695-3746-7 |
Citations | PageRank | References |
7 | 0.68 | 18 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mikolaj Bojanczyk | 1 | 352 | 35.99 |
| Howard Straubing | 2 | 528 | 60.92 |
| Igor Walukiewicz | 3 | 1239 | 90.24 |