@inproceedings{9c49c48693e243d8b725dbb8debe13d6,
title = "Temporal logic with capacity 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 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. {\textcopyright} Springer-Verlag Berlin Heidelberg 2007.",
author = "C. Dixon and M. Fisher and B. Konev",
year = "2007",
doi = "10.1007/978-3-540-74621-8\_11",
language = "English",
isbn = "978-354074620-1",
series = "Lecture Notes in Computer Science",
publisher = "Springer Nature",
pages = "163--177",
booktitle = "Frontiers of Combining Systems",
address = "United States",
note = "FroCoS: International Symposium on Frontiers of Combining Systems : 6th International Symposium ; Conference date: 10-09-2007 Through 12-09-2007",
}