Title :
Parametric quantitative temporal reasoning
Author :
Emerson, E. Allen ; Trefler, Richard J.
Author_Institution :
Dept. of Comput. Sci., Texas Univ., Austin, TX, USA
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 generalised to allow quantitative reasoning about the number of occurrences of atomic events
Keywords :
formal specification; polynomials; temporal logic; temporal reasoning; timing; atomic events; model checking algorithm; parameterized real-time computation tree logic; parametric quantitative temporal reasoning; polynomial; quantitative reasoning; quantitative temporal specifications; temporal ordering; Atomic measurements; Concrete; Contracts; Delay effects; Logic; Polynomials; Process design; Time measurement; Timing;
Conference_Titel :
Logic in Computer Science, 1999. Proceedings. 14th Symposium on
Conference_Location :
Trento
Print_ISBN :
0-7695-0158-3
DOI :
10.1109/LICS.1999.782628
