Combining temporal specification techniques

descriptionPublicationkeyboard_double_arrow_right Part of book or chapter of book , Conference object , Other literature type 23 Nov 2005 English Publisher:Springer Science and Business Media LLC

Authors: Morten Ulrik Sørensen; Odd Erik Hansen; Hans Henrik Løvengreen;

doi: 10.1007/bfb0013977

Combining temporal specification techniques

- Summary
- Metrics

Abstract

This article presents a combination of different temporal specification and verification techniques for real time systems. We develop a semantic model that can be used as a model for both transition based formalisms like TLA and the temporal logics by Manna and Pnueli as well as interval based formalisms like the Duration Calculus. On this model a new temporal logic, TLD, is defined, which combines the strengths of both kinds of formalisms by including all the essential operators of all the considered logics, the meaning of the operators being preserved. Finally, a general framework for relating logics is established, and we prove that TLD is indeed an extension of both DC and TLA.

Related Organizations

Technical University of Denmark
Denmark

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	2
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average