Linear-Time Temporal Logic
摘要
In this chapter we study another logic interpreted over infinite words. It differs from MSO fundamentally in that there are no quantifiers for sets of positions and consequently no variables either. Instead it obtains reasonable expressiveness through the use of temporal operators which is also where the name temporal logic derives from.