Advertisement

Minimizing the Number of Opinions for Fault-Tolerant Distributed Decision Using Well-Quasi Orderings

  • Pierre Fraigniaud
  • Sergio RajsbaumEmail author
  • Corentin Travers
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9644)

Abstract

The notion of deciding a distributed language \(\mathcal {L} \) is of growing interest in various distributed computing settings. Each process \(p_i\) is given an input value \(x_i\), and the processes should collectively decide whether their set of input values \(x=(x_i)_i\) is a valid state of the system w.r.t. to some specification, i.e., if \(x\in \mathcal {L} \). In non-deterministic distributed decision each process \(p_i\) gets a local certificate \(c_i\) in addition to its input \(x_i\). If the input \(x\in \mathcal {L} \) then there exists a certificate \(c=(c_i)_i\) such that the processes collectively accept x, and if \(x\not \in \mathcal {L} \), then for every c, the processes should collectively reject x. The collective decision is expressed by the set of opinions emitted by the processes.

In this paper we study non-deterministic distributed decision in systems where asynchronous processes may crash. It is known that the number of opinions needed to deterministically decide a language can grow with n, the number of processes in the system. We prove that every distributed language \(\mathcal {L} \) can be non-deterministically decided using only three opinions, with certificates of size \(\lceil \log \alpha (n)\rceil +1\) bits, where \(\alpha \) grows at least as slowly as the inverse of the Ackerman function. The result is optimal, as we show that there are distributed languages that cannot be decided using just two opinions, even with arbitrarily large certificates.

To prove our upper bound, we introduce the notion of distributed encoding of the integers, that provides an explicit construction of a long bad sequence in the well-quasi-ordering \((\{0,1\}^*,\le _*)\) controlled by the successor function. Thus, we provide a new class of applications for well-quasi-orderings that lies outside logic and complexity theory. For the lower bound we use combinatorial topology techniques.

Keywords

Runtime verification Distributed decision Distributed verification Well-quasi-ordering Wait-free computing Combinatorial topology 

Notes

Acknowledgment

The third author is thankful to Philippe Duchon and Patrick Dehornoy for fruitful discussions on wqos.

References

  1. 1.
    Afek, Y., Attiya, H., Dolev, D., Gafni, E., Merritt, M., Shavit, N.: Atomic snapshots of shared memory. J. ACM 40(4), 873–890 (1993)CrossRefzbMATHGoogle Scholar
  2. 2.
    Attiya, H., Welch, J.: Distributed Computing: Fundamentals, Simulations, and Advanced Topics. Wiley, Chichester (2004)CrossRefzbMATHGoogle Scholar
  3. 3.
    Bauer, A., Leucker, M., Schallhart, C.: Comparing LTL semantics for runtime verification. J. Log. Comput. 20(3), 651–674 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Blin, L., Fraigniaud, P., Patt-Shamir, B.: On proof-labeling schemes versus silent self-stabilizing algorithms. In: Felber, P., Garg, V. (eds.) SSS 2014. LNCS, vol. 8756, pp. 18–32. Springer, Heidelberg (2014)Google Scholar
  5. 5.
    Chandra, T., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88–98 (2011)CrossRefGoogle Scholar
  7. 7.
    Sarma, A., Holzer, S., Kor, L., Korman, A., Nanongkai, D., Pandurangan, G., Peleg, D., Wattenhofer, R.: Distributed verification and hardness of distributed approximation. SIAM J. Comput. 41(5), 1235–1265 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with dickson’s lemma. In: Proceedings of 26th IEEE Symposium on Logic in Computer Science (LICS), pp. 269–278 (2011)Google Scholar
  9. 9.
    Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374–382 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Fraigniaud, P., Korman, A., Peleg, D.: Towards a complexity theory for local distributed computing. J. ACM 60(5), 35 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Fraigniaud, P., Rajsbaum, S., Travers, C.: Locality and checkability in wait-free computing. Distrib. Comput. 26(4), 223–242 (2013)CrossRefzbMATHGoogle Scholar
  12. 12.
    Fraigniaud, P., Rajsbaum, S., Travers, C.: Minimizing the Number of Opinions for Fault-Tolerant Distributed Decision Using Well-Quasi Orderings Technical report #hal-01237873 (2015). https://hal.archives-ouvertes.fr/hal-01237873v1
  13. 13.
    Fraigniaud, P., Rajsbaum, S., Travers, C.: On the number of opinions needed for fault-tolerant run-time monitoring in distributed systems. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 92–107. Springer, Heidelberg (2014)Google Scholar
  14. 14.
    Fraigniaud, P., Rajsbaum, S., Roy, M., Travers, C.: The opinion number of set-agreement. In: Aguilera, M.K., Querzoni, L., Shapiro, M. (eds.) OPODIS 2014. LNCS, vol. 8878, pp. 155–170. Springer, Heidelberg (2014)Google Scholar
  15. 15.
    Göös, M., Suomela, J.: Locally checkable proofs. In: Proceedings of 30th ACM Symposium on Principles of Distributed Computing (PODC), pp. 159–168 (2011)Google Scholar
  16. 16.
    Haase, C., Schmitz, S., Schnoebelen, P.: The power of priority channel systems. In: D’Argenio, P.R., Melgratti, H. (eds.) CONCUR 2013 – Concurrency Theory. LNCS, vol. 8052, pp. 319–333. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  17. 17.
    Herlihy, M., Kozlov, D., Rajsbaum, S.: Distributed Computing Through Combinatorial Topology. Morgan Kaufmann (2013)Google Scholar
  18. 18.
    Jeanmougin, M.: Checkability in Asynchronous Error-Prone Distributed Computing Using Few Values. Master Thesis Report, University Paris Diderot (2013)Google Scholar
  19. 19.
    Korman, A., Kutten, S., Peleg, D.: Proof labeling schemes. Distrib. Comput. 22(4), 215–233 (2010)CrossRefzbMATHGoogle Scholar
  20. 20.
    Kruskal, J.: The theory of well-quasi-ordering: a frequently discovered concept. J. Comb. Theor. A 13(3), 297–305 (1972)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Milner, E.: Basic WQO- and BQO-theory. In: Rival, I. (ed.) The Role of Graphs in the Theory of Ordered Sets and Its Applications. NATO ASI Series, vol. 147, pp. 487–502. Springer, Netherlands (1985)Google Scholar
  22. 22.
    Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of IEEE Parallel and Distributed Processing Symposium (IPDPS), pp. 494–503 (2015)Google Scholar
  23. 23.
    Schmitz, S., Schnoebelen, P.: Multiply-recursive upper bounds with higman’s lemma. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 441–452. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  24. 24.
    Schmitz, S., Schnoebelen, P.: Algorithmic Aspects of WQO Theory. Technical report Hal#cel-00727025 (2013). https://cel.archives-ouvertes.fr/cel-00727025v2
  25. 25.
    Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251–261 (2002)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Schnoebelen, P.: Revisiting ackermann-hardness for lossy counter machines and reset petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  27. 27.
    Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69 (1949)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2016

Authors and Affiliations

  • Pierre Fraigniaud
    • 1
  • Sergio Rajsbaum
    • 2
    Email author
  • Corentin Travers
    • 3
  1. 1.University Paris Diderot and CRNSParisFrance
  2. 2.Instituto de Matemáticas, UNAMMexico CityMexico
  3. 3.University of BordeauxTalenceFrance

Personalised recommendations