Skip to content Skip to navigation
University of Warwick
  • Study
  • |
  • Research
  • |
  • Business
  • |
  • Alumni
  • |
  • News
  • |
  • About

University of Warwick
Publications service & WRAP

Highlight your research

  • WRAP
    • Home
    • Search WRAP
    • Browse by Warwick Author
    • Browse WRAP by Year
    • Browse WRAP by Subject
    • Browse WRAP by Department
    • Browse WRAP by Funder
    • Browse Theses by Department
  • Publications Service
    • Home
    • Search Publications Service
    • Browse by Warwick Author
    • Browse Publications service by Year
    • Browse Publications service by Subject
    • Browse Publications service by Department
    • Browse Publications service by Funder
  • Statistics
  • Help & Advice
University of Warwick

The Library

  • Login

Two-sorted metric temporal logics

Tools
- Tools
+ Tools

UNSPECIFIED (1997) Two-sorted metric temporal logics. In: 4th Biennial Conference on Algebraic Methodology and Software Technology (AMAST 95), JUL 03-07, 1995, MONTREAL, CANADA.

Full text not available from this repository.

Abstract

Temporal logic has been successfully used for modeling and analyzing the behavior of reactive and concurrent systems. Standard temporal logic is inadequate for real-time applications because it only deals with qualitative timing properties. This is overcome by metric temporal logics which offer a uniform logical framework in which both qualitative and quantitative timing properties can be expressed by making use of a parameterized operator of relative temporal realization. In this paper we deal with completeness issues for basic systems of metric temporal logic despite their relevance, such issues have been ignored or only partially addressed in the literature. We view metric temporal logics as two-sorted formalisms having formulae ranging over time instants and parameters ranging over an (ordered) abelian group of temporal displacements. We first provide an axiomatization of the pure metric fragment of the logic, and prove its soundness and completeness. Then, we show how to obtain the metric temporal logic of linear orders by adding an ordering over displacements. Finally, we consider general metric temporal logics allowing quantification over algebraic variables and free mixing of algebraic formulae and temporal propositional symbols.

Item Type: Conference Item (UNSPECIFIED)
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Journal or Publication Title: THEORETICAL COMPUTER SCIENCE
Publisher: ELSEVIER SCIENCE BV
ISSN: 0304-3975
Date: 15 September 1997
Volume: 183
Number: 2
Number of Pages: 28
Page Range: pp. 187-214
Publication Status: Published
Title of Event: 4th Biennial Conference on Algebraic Methodology and Software Technology (AMAST 95)
Location of Event: MONTREAL, CANADA
Date(s) of Event: JUL 03-07, 1995
URI: http://wrap.warwick.ac.uk/id/eprint/16417

Data sourced from Thomson Reuters' Web of Knowledge

Request changes to a record

Actions (login required)

View Item View Item
twitter

Email us: publications@warwick.ac.uk
Contact Details
About Us