Temporal Reasoning in Bounded Situation Calculus

In this talk, we survey recent results on situation calculus bounded action theories. These are action theories with the constraints that the size of the extension of fluents in every situation must be bounded, though such an extension changes from situation to situation. Such action theories give rise to infinite transition systems that can be faithfully abstracted into finite ones, making verification decidable.