Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Decidable classes of the verification problem in a timed predicate logic

Danièle BeauquierContact Information and Anatol SlissenkoContact Information

(6)  Dept. of Informatics, University Paris-12, 61 Av. du Gèn. de Gaulle, 94010 Crèteil, France
Abstract
We consider a first order timed logic that is an extension of the theory of real addition and scalar multiplications (by rational numbers) by unary functions and predicates of time. The time is treated as non negative reals. This logic seems to be well adapted to a direct, full-scale specification of real-time systems. It also suffices to describe runs of timed algorithms that have as inputs functions of time. Thus it permits to embed the verification of timed systems in one easily understandable framework. But this logic is incomplete, and hence undecidable. To develop an algorithmic support for the verification problem one theoretical direction of research is to look for reasonable decidable classes of the verification problem. In this paper we describe such classes modeling typical properties of practical systems such as dependence of behavior only on a small piece of history and periodicity.

Contact Information Danièle Beauquier
Email: beauquier@univ-paris12.fr

Contact Information Anatol Slissenko
Email: slissenko@univ-paris12.fr
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.105 • Server: mpweb08
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)