We provide an extension of topological nexttime logic by an operator expressing an increase of sets. The resulting formalism enables one to reason about the change of sets in the course of (discrete) linear time. We establish completeness and decidability of the new system, and determine its complexity. As for the latter, we obtain a 'low' upper complexity bound of the corresponding satisfiability problem: NP; this is due to the fact that the time operators involved in our logic are comparatively weak. It is intended that the system is applicable to diverse fields of temporal reasoning.
展开▼
