Anzeige
Erschienen in:
2007 | OriginalPaper | Buchkapitel
Temporal Logic with Capacity Constraints
verfasst von : Clare Dixon, Michael Fisher, Boris Konev
Erschienen in: Frontiers of Combining Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 paper describes both the logical basis and a verification method for propositional linear time temporal logics which allow such constraints as input. The method incorporates ideas developed earlier for a resolution method for the temporal logic TLX and a tableaux-like procedure for PTL. 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.