Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
436558 | Theoretical Computer Science | 2006 | 18 Pages |
Abstract
The expressive power of temporal branching time logics that use the modalities EX and EF is described. Forbidden pattern characterizations are given for tree languages definable in three logics: EX, EF and EX+EF. The characterizations give algorithms for the definability problem in the respective logics that are polynomial in the size of a deterministic tree automaton representing the language.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics