| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 428295 | Information Processing Letters | 2007 | 7 Pages |
Abstract
In this note, we give a new proof for Bojańczyk and Walukiewicz's effective characterization of TL[EF] (the fragments of Computation Tree Logic (CTL), with EF modality only) following the Ehrenfeucht–Fraïssé game approach. Then, we extend the proof to the effective characterization of TL[EFns] (Fns is the non-strict “future” temporal operator, while F is the strict one).
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
![A note on the characterization of TL[EF]](/preview/png/428295.png "First Page Preview: A note on the characterization of TL[EF]")