Document Open Access Logo

What's Decidable about Availability Languages?

Authors Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, Mehdi Seyed Salehi

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2015.192.pdf
  • Filesize: 495 kB
  • 14 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
Mohamed Faouzi Atig
Roland Meyer
Mehdi Seyed Salehi

Cite AsGet BibTex

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi. What's Decidable about Availability Languages?. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 192-205, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.FSTTCS.2015.192

Abstract

We study here the algorithmic analysis of systems modeled in terms of availability languages. Our first main result is a positive answer to the emptiness problem: it is decidable whether a given availability language contains a word. The key idea is an inductive construction that replaces availability languages with Parikh-equivalent regular languages. As a second contribution, we solve the intersection problem modulo bounded languages: given availability languages and a bounded language, it is decidable whether the intersection of the former contains a word from the bounded language. We show that the problem is NP-complete. The idea is to reduce to satisfiability of existential Presburger arithmetic. Since the (general) intersection problem for availability languages is known to be undecidable, our results characterize the decidability border for this model. Our last contribution is a study of the containment problem between regular and availability languages. We show that safety verification, i.e., checking containment of an availability language in a regular language, is decidable. The containment problem of regular languages in availability languages is proven undecidable.
Keywords
  • Availability
  • formal languages
  • emptiness
  • decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Cadilhac, A. Finkel, and P. McKenzie. On the expressiveness of Parikh automata and related models. arXiv:1101.1547 [cs], 2011. Google Scholar
  2. M. Cadilhac, A. Finkel, and P. McKenzie. Affine Parikh automata. RAI, 46(4):511-545, 2012. Google Scholar
  3. M. Cadilhac, A. Finkel, and P. McKenzie. Bounded Parikh automata. International Journal of Foundations of Computer Science, 23(8):1691-1709, 2012. Google Scholar
  4. E. de Souza e Silva and H. R. Gail. Calculating availability and performability measures of repairable computer systems using randomization. JACM, 36(1):171-193, 1989. Google Scholar
  5. M. Droste, W. Kuich, and H. Vogler, editors. Handbook of Weighted Automata. EATCS Monographs. Springer, 2009. Google Scholar
  6. J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, pages 499-510. ACM, 2011. Google Scholar
  7. J. Esparza, P. Ganty, S. Kiefer, and M. Luttenberger. Parikh’s theorem: A simple and direct automaton construction. IPL, 111(12):614-619, 2011. Google Scholar
  8. P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. FMSD, 40(2):206-231, 2012. Google Scholar
  9. S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematic, 16(2):285-296, 1966. Google Scholar
  10. M. Hague and A. W. Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of LNCS, pages 260-276. Springer, 2012. Google Scholar
  11. J. Hoenicke, R. Meyer, and E.-R. Olderog. Kleene, Rabin, and Scott are available. In CONCUR, number 6269 in LNCS, pages 462-477. Springer, 2010. Google Scholar
  12. F. Klaedtke and H. Rueß. Monadic second-order logics with cardinalities. In ICALP, volume 2719 of LNCS, pages 681-696. Springer, 2003. Google Scholar
  13. M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967. Google Scholar
  14. R. J. Parikh. On context-free languages. JACM, 13(4):570-581, 1966. Google Scholar
  15. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  16. G. Rubino and B. Sericola. Interval availability distribution computation. In Fault-Tolerant Computing, pages 48-55, 1993. Google Scholar
  17. B. Scarpellini. Complexity of subcases of Presburger arithmetic. Transactions of the AMS, 284(1):203-218, 1984. Google Scholar
  18. H. Seidl, T. Schwentick, and A. Muscholl. Numerical document queries. In PODS, pages 155-166. ACM, 2003. Google Scholar
  19. K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational horn clauses. In CADE, volume 3632 of LNCS, pages 337-352. Springer, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact