Deductive Temporal Reasoning with Constraints

Abstract

Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most 'n' processes can access a particular resource at any moment or exactly 'm' participants are needed for an agreement. Such situations are concisely modelled where propositions are constrained such that at most 'n', or exactly 'm', can hold at any moment in time. This talk describes both the logical basis and a verification method for propositional linear time temporal logics which allow such constraints as input. The complexity of this procedure is discussed and case studies are examined. The logic itself represents a combination of standard temporal logic with classical constraints restricting the numbers of propositions that can be satisfied at any moment in time. We discuss restrictions to the general case where only 'exactly one' type constraints are allowed and extensions to first-order temporal logic.