Logic in Computer Science (LICS 1999)

Paper: Parametric Quantitative Temporal Reasoning (at LICS 1999)

Authors: E. Allen Emerson Richard J. Trefler

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.

BibTeX

  @InProceedings{EmersonTrefler-ParametricQuantitat,
    author = 	 {E. Allen Emerson and Richard J. Trefler},
    title = 	 {Parametric Quantitative Temporal Reasoning},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {336--343},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }