On termination and invariance for faulty channel machines

详细信息    查看全文

• 作者：Patricia Bouyer (1)
  Nicolas Markey (1)
  Jo?l Ouaknine (2)
  Philippe Schnoebelen (1)
  James Worrell (2) jbw@cs.ox.ac.uk
• 关键词：Channel machines – Computational complexity – Metric temporal logic – Primitive recursive – Well ; structured systems
• 刊名：Formal Aspects of Computing
• 出版年：2012
• 出版时间：July 2012
• 年：2012
• 卷：24
• 期：4-6
• 页码：595-607
• 全文大小：410.5 KB
• 参考文献：1. Abdulla PA, ?erans K, Jonsson B, Tsay Y-K (2000) Algorithmic analysis of programs with well quasi-ordered domains. Inf Comput 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, Jonsson B (1996) Undecidable verification problems for programs with unreliable channels. Inf Comput 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, Zafiropulo P (1983) On communicating finite-state machines. J ACM 30(2): 323–342
  7. Cécé G, Finkel A, Purushothaman Iyer S (1996) Unreliable channels are easier to verify than perfect channels. Inf Comput 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 (1994) Decidability of the termination problem for completely specificied protocols. Distrib Comput 7(3): 129–135
  10. Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1–2): 63–92
  11. Higman G (1952) Ordering by divisibility in abstract algebras. Proc Lond Math Soc 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, Ullman JD (1979) Introduction to automata theory, languages and computation. Addison-Wesley, Boston
  14. Koymans R (1990) Specifying real-time properties with metric temporal logic. Real Time Syst 2(4): 255–299
  15. Lazi? R (2011) Safety alternating automata on data words. ACM Trans Comput Log 12(2): 10
  16. Lazi? R, Newcomb T, Ouaknine J, Roscoe AW, Worrell J (2008) Nets with tokens which carry data Fundam Inf 88(3): 251–274
  17. Lasota S, Walukiewicz I (2008) Alternating timed automata. ACM Trans Comput Log 9(2)
  18. Mayr R (2003) Undecidable problems in unreliable computations. Theor Comput Sci 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 (1978) The covering and boundedness problems for vector addition systems. Theor Comput Sci 6(2): 223–231
  23. Schnoebelen P (2002) Verifying lossy channel systems has nonprimitive recursive complexity. Inf Process Lett 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
• 作者单位：1. LSV, ENS Cachan, CNRS, Cachan, France2. Department of Computer Science, Oxford University, Oxford, UK
• ISSN：1433-299X

文摘

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.