Name
Abstract | ||
|---|---|---|
Often when modelling systems, physical constraints on the resources available are needed. For example, we might say that at most Nprocesses can access a particular resource at any moment or exactly Mparticipants 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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1007/978-3-540-74621-8_11 | FroCos |
Keywords | Field | DocType |
capacity constraints,temporal logic,standard temporal logic,resolution method,classical constraint,tableaux-like procedure,propositional linear time,modelling system,verification method,logical basis,case study | Computation tree logic,Discrete mathematics,Temporal logic of actions,Interval temporal logic,Computer science,Algorithm,Zeroth-order logic,Multimodal logic,Linear temporal logic,Temporal logic,Time complexity | Conference |
Volume | ISSN | Citations |
4720 | 0302-9743 | 3 |
PageRank | References | Authors |
0.38 | 15 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Clare Dixon | 1 | 552 | 42.94 |
| Michael Fisher | 2 | 691 | 49.23 |
| Boris Konev | 3 | 569 | 42.08 |