We give several new applications of the wreath product of forest algebras to the study of logics on trees. These include new simplified proofs of necessary conditions for definability in CTL and first-order logic with the ancestor relation; a sequence of identities satisfied by all forest languages definable in PDL; and new examples of languages outside CTL, along with an application to the question of what properties are definable in both CTL and LTL.
Mots-clés : tree automata, temporal logics, forest algebras
@article{ITA_2013__47_3_261_0, author = {Straubing, Howard}, title = {New applications of the wreath product of forest algebras}, journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications}, pages = {261--291}, publisher = {EDP-Sciences}, volume = {47}, number = {3}, year = {2013}, doi = {10.1051/ita/2013039}, mrnumber = {3103128}, language = {en}, url = {http://www.numdam.org/articles/10.1051/ita/2013039/} }
TY - JOUR AU - Straubing, Howard TI - New applications of the wreath product of forest algebras JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications PY - 2013 SP - 261 EP - 291 VL - 47 IS - 3 PB - EDP-Sciences UR - http://www.numdam.org/articles/10.1051/ita/2013039/ DO - 10.1051/ita/2013039 LA - en ID - ITA_2013__47_3_261_0 ER -
%0 Journal Article %A Straubing, Howard %T New applications of the wreath product of forest algebras %J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications %D 2013 %P 261-291 %V 47 %N 3 %I EDP-Sciences %U http://www.numdam.org/articles/10.1051/ita/2013039/ %R 10.1051/ita/2013039 %G en %F ITA_2013__47_3_261_0
Straubing, Howard. New applications of the wreath product of forest algebras. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 47 (2013) no. 3, pp. 261-291. doi : 10.1051/ita/2013039. http://www.numdam.org/articles/10.1051/ita/2013039/
[1] Regular tree languages definable in fo and in fomod. ACM Trans. Comput. Logic 11 (2009) 1-4. | MR | Zbl
and ,[2] Algebra for trees, in AutoMathA Handbook, edited by J.-E. Pin (2012). Preprint.
,[3] Forest algebras, in Logic and Automata: History and Perspectives, edited by E. Graedel, J. Flum and T. Wilke. Amsterdam University Press (2008). | MR | Zbl
and ,[4] Decidable Properties of Tree Languages. Ph.D. thesis, University of Warsaw (2004).
,[5] The common fragment of actl and ltl. In FoSSaCS, vol. 4962 of Lect. Notes Comput Sci., edited by R.M. Amadio (2008) 172-185. | MR | Zbl
,[6] Piecewise testable tree languages. To appear in Logical Methods Comput. Sci. (2012). | MR | Zbl
, and ,[7] Wreath products of forest algebras, with applications to tree logics. To appear in Logical Methods Comput. Sci. (2012). | MR | Zbl
, and ,[8] Automata, Languages, and Machines, vol. B. Pure and Applied Mathematics. New York, Academic Press (1976). | MR | Zbl
,[9] Temporal and modal logic, in Handbook Of Theoretical Computer Science. Elsevier (1995) 995-1072. | MR | Zbl
,[10] Elements Of Finite Model Theory. Texts in Theoretical Computer Science. Springer (2004). | MR | Zbl
,[11] The common fragment of ctl and ltl. In FOCS. IEEE Computer Society (2000) 643-652. | MR
,[12] On the expressive power of ctl. In LICS. IEEE Computer Society (1999) 360-368. | MR | Zbl
and ,[13] Varieties of formal languages. North Oxford Academic (1986). | MR | Zbl
,[14] Syntactic semigroups, vol. 1 in Handbook of Formal Languages. Springer (1997). | MR
,[15] First-order logic on finite trees. Lect. Notes Comput. Sci. 915 (1995) 125-139.
,[16] Sur le produit de concatenation non ambigu. Semigroup Forum 13 (1976) 47-75. Doi: 10.1007/BF02194921. | EuDML | MR | Zbl
,[17] Branching-depth hierarchies. Electr. Notes Theor. Comput. Sci. 39 (2000) 65-78. | Zbl
, and ,Cité par Sources :