A decidable timeout-based extension of linear temporal logic


Abstract
We develop a timeout extension of propositional linear temporal logic to specify timing properties of timeout-based models of real-time systems. A timeout is used to model the execution of an action marking the end of a delay. With a view to expressing such timeout constraints, ToLTL uses a dynamic variable to abstract the timeout behaviour in addition to a variable which captures the global clock and some static timing variables which record time instances when discrete events occur. We propose a corresponding timeout tableau for satisfiability checking of the ToLTL formulas. Further we prove that the validity checking for such an extended logic remains PSPACE-complete. Under discrete time semantics, with bounded timeout increments, the model-checking problem which verifies if a ToLTL-formula holds in a timeout Kripke structure is also shown to be PSPACE complete. We further prove that ToLTL, when interpreted over discrete time, can be embedded in the monadic second-order logic with..
Keywords No keywords specified (fix it)
Categories (categorize this paper)
ISBN(s)
DOI 10.1080/11663081.2014.964491
Options
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: 44,462
Through your library

References found in this work BETA

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Reasoning Processes in Propositional Logic.Claes Strannegård, Simon Ulfsbäcker, David Hedqvist & Tommy Gärling - 2010 - Journal of Logic, Language and Information 19 (3):283-314.
A Logic for Metric and Topology.Frank Wolter & Michael Zakharyaschev - 2005 - Journal of Symbolic Logic 70 (3):795 - 828.
Linear, Branching Time and Joint Closure Semantics for Temporal Logic.Joeri Engelfriet & Jan Treur - 2002 - Journal of Logic, Language and Information 11 (4):389-425.
Complexity, Decidability and Completeness.Douglas Cenzer & Jeffrey B. Remmel - 2006 - Journal of Symbolic Logic 71 (2):399 - 424.
Adding a Temporal Dimension to a Logic System.Marcelo Finger & Dov M. Gabbay - 1992 - Journal of Logic, Language and Information 1 (3):203-233.
Logical Consecutions in Discrete Linear Temporal Logic.V. V. Rybakov - 2005 - Journal of Symbolic Logic 70 (4):1137 - 1149.
An Event-Based Fragment of First-Order Logic Over Intervals.Savas Konur - 2011 - Journal of Logic, Language and Information 20 (1):49-68.

Analytics

Added to PP index
2014-11-11

Total views
15 ( #561,898 of 2,273,201 )

Recent downloads (6 months)
1 ( #826,598 of 2,273,201 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature