A formal logic of plans in temporally rich domains

This paper outlines a temporal logic extended with two modalities that can be used to support planning in temporally rich domains. In particular, the logic can represent planning environments that have assertions about future possibilities in addition to the present state, and plans that contain concurrent actions. The logic is particularly expressive in the ways that concurrent actions can interact with each other and allows situations where either one of the actions can be executed, but both cannot, as well as situations where neither action can be executed alone, but they can be done together. Two modalities are introduced and given a formal semantics: INEV expresses simple temporal possibility, and IFTRIED expresses counteffactual-like statements about actions.