Parametric quantitative temporal reasoning

20 January 2003

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

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.

Keywords

This publication has 17 references indexed in Scilit:

RuleBase: an industry-oriented formal verification tool
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2005
Design and synthesis of synchronization skeletons using branching time temporal logic
Published by Springer Nature ,2005
Generalized quantitative temporal reasoning: An automata-theoretic approach
Published by Springer Nature ,1997
Parametric real-time reasoning
Published by Association for Computing Machinery (ACM) ,1993
Real-time and the Mu-Calculus (preliminary report)
Published by Springer Nature ,1992
Logics and models of real time: A survey
Published by Springer Nature ,1992
A really temporal logic
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1989
Safety analysis of timing properties in real-time systems
IEEE Transactions on Software Engineering, 1986
On the Development of Reactive Systems
Published by Springer Nature ,1985
The temporal logic of programs
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1977