Name
Abstract | ||
|---|---|---|
We define Parameterized Real-Time Computation Tree Logic (PRTCTL), which allows quantitative temporal specifications to be parameterized over the natural numbers. Parameterized quantitative specifications are quantitative specifications in which concrete timing information has been abstracted away. Such abstraction allows designers to specify quantitative restrictions on the temporal ordering of events without having to use specific timing information from the model. A model checking algorithm for the logic is given which is polynomial for any fixed number of parameters. A subclass of formulae are identified for which the model checking problem is linear in the length of the formula and size of the structure. PRTCTL is generalized to allow quantitative reasoning about the number of occurrences of atomic events. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1109/LICS.1999.782628 | LICS |
Keywords | Field | DocType |
parameterized quantitative specification,parametric quantitative temporal reasoning,quantitative temporal specification,natural number,model checking algorithm,model checking problem,fixed number,quantitative specification,quantitative restriction,quantitative reasoning,concrete timing information,process design,polynomial,formal specification,atomic events,time measurement,polynomials,real time,logic,concrete,temporal logic | Computation tree logic,Discrete mathematics,Parameterized complexity,Model checking,Polynomial,Computer science,Algorithm,Theoretical computer science,Formal specification,Parametric statistics,Temporal logic,Qualitative reasoning | Conference |
ISBN | Citations | PageRank |
0-7695-0158-3 | 41 | 1.67 |
References | Authors | |
12 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| e allen emerson | 1 | 7683 | 1183.13 |
| Richard J. Trefler | 2 | 222 | 14.59 |