Algebra for Infinite Forests with an Application to the Temporal Logic EF

We define an extension of forest algebra for -forests. We show how the standard algebraic notions (free object, syntactic algebra, morphisms, etc.) extend to the infinite case. To prove its usefulness, we use the framework to get an effective characterization of the -forest languages that are definable in the temporal logic that uses the operator EF (exists finally).

• Type: Conference
• Year: 2009
• Where: CONCUR
• Authors: Mikolaj Bojanczyk, Tomasz Idziaszek
• Keywords: CONCUR 2009, Distributed And Parallel Computing, Forest Algebra, Standard Algebraic Notions, Syntactic Algebra