Cited By
View all- Hampson C(2019)On the Termination Problem for Counter Machines with Incrementing ErrorsReachability Problems10.1007/978-3-030-30806-3_11(137-148)Online publication date: 11-Sep-2019
On termination and invariance for faulty channel machines
Authors: 
Patricia Bouyer, Nicolas Markey, Joël Ouaknine, Philippe Schnoebelen, James WorrellAuthors Info & Claims
Pages 595 - 607
Abstract
A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. We consider the invariance problem: does a given insertion channel machine have an infinite computation all of whose configurations satisfy a given predicate? We show that this problem is primitive-recursive if the predicate is closed under message losses. We also give a non-elementary lower bound for the invariance problem under this restriction. Finally, using the previous result, we show that the satisfiability problem for the safety fragment of Metric Temporal Logic is non-elementary.
References
References
[1]
Abdulla PA, Čerans K, Jonsson B, and Tsay Y-K Algorithmic analysis of programs with well quasi-ordered domains Inf Comput 2000 160 1/2 109-127
[2]
Abdulla PA, Jonsson B (1993) Verifying programs with unreliable channels. In: Proceedings of LICS ’93. IEEE Computer Society Press, New York, pp 160–170
[3]
Abdulla PA and Jonsson B Undecidable verification problems for programs with unreliable channels Inf Comput 1996 130 1 71-90
[4]
Baier C, Bertrand N, Schnoebelen P (2006) On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In: Proceedings of LPAR 2006. Lecture Notes in Artificial Intelligence, vol 4246. Springer, Berlin, pp 347–361
[5]
Bouyer P, Markey N, Ouaknine J, Schnoebelen P, Worrell J (2008) On termination for faulty channel machines. In: Proceedings of STACS 2008. LIPIcs, vol 1. Schloß Dagstuhl-Leibniz-Zentrum für Informatik, pp 121–132
[6]
Brand D and Zafiropulo P On communicating finite-state machines J ACM 1983 30 2 323-342
[7]
Cécé G, Finkel A, and Purushothaman Iyer S Unreliable channels are easier to verify than perfect channels Inf Comput 1996 124 1 20-31
[8]
Chambart P, Schnoebelen P (2008) The ordinal recursive complexity of lossy channel systems. In: Proceedings of LICS 2008. IEEE Computer Society, New York, pp 205–216
[9]
Finkel A Decidability of the termination problem for completely specificied protocols Distrib Comput 1994 7 3 129-135
[10]
Finkel A and Schnoebelen P Well-structured transition systems everywhere! Theor Comput Sci 2001 256 1–2 63-92
[11]
Higman G Ordering by divisibility in abstract algebras Proc Lond Math Soc 1952 2 7 326-336
[12]
Henzinger TA, Manna Z, Pnueli A (1992) What good are digital clocks? In: Proceedings of 19th international colloquium on automata, languages and programming (ICALP’92). Lecture Notes in Computer Science, vol 623. Springer, Berlin, pp 545–558
[13]
Hopcroft JE and Ullman JD Introduction to automata theory, languages and computation 1979 Boston Addison-Wesley
[14]
Koymans R Specifying real-time properties with metric temporal logic Real Time Syst 1990 2 4 255-299
[15]
Lazić R Safety alternating automata on data words ACM Trans Comput Log 2011 12 2 10
[16]
Lazić R, Newcomb T, Ouaknine J, Roscoe AW, and Worrell J Nets with tokens which carry data Fundam Inf 2008 88 3 251-274
[17]
Lasota S, Walukiewicz I (2008) Alternating timed automata. ACM Trans Comput Log 9(2)
[18]
Mayr R Undecidable problems in unreliable computations Theor Comput Sci 2003 297 1 35-65
[19]
Ouaknine J, Worrell J (2005) On the decidability of metric temporal logic. In: Proceedings of LICS 2005. IEEE Computer Society Press, New York, pp 188–197
[20]
Ouaknine J, Worrell J (2006) On metric temporal logic and faulty Turing machines. In: Proceedings of FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, pp 217–230
[21]
Ouaknine J, Worrell J (2006) Safety metric temporal logic is fully decidable. In: Proceedings of TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, pp 411–425
[22]
Rackoff C The covering and boundedness problems for vector addition systems Theor Comput Sci 1978 6 2 223-231
[23]
Schnoebelen P Verifying lossy channel systems has nonprimitive recursive complexity Inf Process Lett 2002 83 5 251-261
[24]
Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time: preliminary report. In: Proceedings of STOC ’73. ACM, New York, pp 1–9
[25]
Schmitz S, Schnoebelen P (2011) Multiply-recursive upper bounds with Higman’s lemma. In: Proceedings of ICALP 2011. Lecture Notes in Computer Science, vol 6756. Springer, Berlin, pp 441–452
Recommendations
Zeno, Hercules, and the Hydra: Safety Metric Temporal Logic is Ackermann-Complete
Metric temporal logic (MTL) is one of the most prominent specification formalisms for real-time systems. Over infinite timed words, full MTL is undecidable, but satisfiability for a syntactially defined safety fragment, called safety MTL, was proved ...
Precoding methods for multi‐input multi‐ouput interference channels with channel covariance Feedback
Usually, instantaneous channel information is required by the transmitter for the precoding in multi‐input multi‐output interference channels. In the case of fast fading channels, the resultant additional overhead of the system will be high. Against this, ...
A tensor-based approach for frequency-selective MIMO channel equalization
AbstractIn this paper, a novel tensor-based method is proposed to equalize frequency-selective multiple-input multiple-output (FS-MIMO) channels. Since both the spatial and temporal aspects of such channels are considered in the proposed method at the ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© British Computer Society 2012.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 July 2012
Accepted: 02 May 2012
Revision received: 25 April 2012
Received: 21 December 2011
Published in FAC Volume 24, Issue 4-6
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 53Total Downloads
- Downloads (Last 12 months)25
- Downloads (Last 6 weeks)9
Reflects downloads up to 25 Nov 2024
Other Metrics
Citations
Cited By
View all- Hampson C(2019)On the Termination Problem for Counter Machines with Incrementing ErrorsReachability Problems10.1007/978-3-030-30806-3_11(137-148)Online publication date: 11-Sep-2019
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in