Article ID Journal Published Year Pages File Type
4662609 Annals of Pure and Applied Logic 2006 32 Pages PDF
Abstract

We show that the satisfiability problem for the monodic guarded, loosely guarded, and packed fragments of first-order temporal logic with equality is 2Exptime-complete for structures with arbitrary first-order domains, over linear time, dense linear time, rational number time, and some other classes of linear flows of time. We then show that for structures with finite first-order domains, these fragments are also 2Exptime-complete over real number time and hence over most of the commonly used linear flows of time, including the natural numbers, integers, rationals, and any first-order definable class of linear flows of time.

Related Topics
Physical Sciences and Engineering Mathematics Logic