A first order logic for specification of timed algorithms: basic properties and a decidable class

Annals of Pure and Applied Logic 113 (1-3):13-52 (2001)
We consider one aspect of the problem of specification and verification of reactive real-time systems which involve operations and constraints concerning time. Time is continuous what is motivated by specifications of hybrid systems. Our goal is to try to find a framework that is based on applied first order logic that permits to represent the verification problem directly, completely and conservatively , and that is apt to describe interesting decidable classes, maybe showing way to feasible algorithms. To achieve this goal we use a first order timed logic that is an extension of a decidable theory of reals with timed functions. This logic permits, on the one hand, to rewrite directly and completely requirements and, on the other hand, to describe executions of various timed algorithms—here we consider block Gurevich abstract state machines because of their theoretical clarity and sufficient expressive power. Then we describe one decidable class of the verification problem that is based on notions reflecting finiteness properties of systems of control. These notions may be of independent interest, as, in particular, they give a way to describe a limited usage of arithmetics preserving decidability that is not covered by existing model-theoretic approaches. As an example we consider the generalized railroad crossing problem that we analyze in its entirety
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/S0168-0072(01)00049-5
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 35,496
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

Decidable Properties for Monadic Abstract State Machines.Daniele Beauquier - 2006 - Annals of Pure and Applied Logic 141 (3):308-319.

Add more citations

Similar books and articles

Timed Modal Logics for Real-Time Systems.Patricia Bouyer, Franck Cassez & François Laroussinie - 2011 - Journal of Logic, Language and Information 20 (2):169-203.
Pure Second-Order Logic with Second-Order Identity.Alexander Paseau - 2010 - Notre Dame Journal of Formal Logic 51 (3):351-360.
Constructive Interpolation in Hybrid Logic.Patrick Blackburn & Maarten Marx - 2003 - Journal of Symbolic Logic 68 (2):463-480.
Decidable Properties for Monadic Abstract State Machines.Daniele Beauquier - 2006 - Annals of Pure and Applied Logic 141 (3):308-319.
An Undecidable Linear Order That Is $N$-Decidable for All $N$.John Chisholm & Michael Moses - 1998 - Notre Dame Journal of Formal Logic 39 (4):519-526.
On Logic of Complex Algorithms.Helena Rasiowa - 1981 - Studia Logica 40 (3):289 - 310.
Order.Vincent Stuart (ed.) - 1977 - Random House.


Added to PP index

Total downloads
2 ( #933,813 of 2,287,477 )

Recent downloads (6 months)
1 ( #389,932 of 2,287,477 )

How can I increase my downloads?

Monthly downloads

My notes

Sign in to use this feature