Document Open Access Logo

Parameterized Communicating Automata: Complementation and Model Checking

Authors Benedikt Bollig, Paul Gastin, Akshay Kumar

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.625.pdf
  • Filesize: 1.07 MB
  • 13 pages

Document Identifiers

Author Details

Benedikt Bollig
Paul Gastin
Akshay Kumar

Cite As Get BibTex

Benedikt Bollig, Paul Gastin, and Akshay Kumar. Parameterized Communicating Automata: Complementation and Model Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 625-637, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014) https://doi.org/10.4230/LIPIcs.FSTTCS.2014.625

Abstract

We study the language-theoretical aspects of parameterized communicating automata (PCAs), in which processes communicate via rendez-vous. A given PCA can be run on any topology of bounded degree such as pipelines, rings, ranked trees, and grids. We show that, under a context bound, which restricts the local behavior of each process, PCAs are effectively complementable. Complementability is considered a key aspect of robust automata models and can, in particular, be exploited for verification. In this paper, we use it to obtain a characterization of context-bounded PCAs in terms of monadic second-order (MSO) logic. As the emptiness problem for context-bounded PCAs is decidable for the classes of pipelines, rings, and trees, their model-checking problem wrt. MSO properties also becomes decidable. While previous work on model checking parameterized systems typically uses temporal logics without next operator, our MSO logic allows one to express several natural next modalities.

Subject Classification

Keywords
  • parameterized verification
  • complementation
  • monadic second-order logic

Metrics

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

References

  1. P. A. Abdulla, F. Haziza, and L. Holík. All for the price of few. In VMCAI'13, volume 7737 of LNCS, pages 476-495. Springer, 2013. Google Scholar
  2. B. Aminof, S. Jacobs, A. Khalimov, and S. Rubin. Parameterized model checking of token-passing systems. In VMCAI'14, volume 8318 of LNCS, pages 262-281. Springer, 2014. Google Scholar
  3. B. Bollig. Logic for communicating automata with parameterized topology. In CSL-LICS'14. ACM Press, 2014. Google Scholar
  4. B. Bollig, P. Gastin, and J. Schubert. Parameterized Verification of Communicating Automata under Context Bounds. In RP'14, volume 8762 of LNCS, pages 45-57, 2014. Google Scholar
  5. D. Brand and P. Zafiropulo. On communicating finite-state machines. J. ACM, 30(2), 1983. Google Scholar
  6. G. Delzanno, A. Sangnier, and G. Zavattaro. On the power of cliques in the parameterized verification of ad hoc networks. In FoSSaCS'11, volume 6604 of LNCS, pages 441-455. Springer, 2011. Google Scholar
  7. E. A. Emerson and K. S. Namjoshi. On reasoning about rings. Int. J. Found. Comput. Sci., 14(4):527-550, 2003. Google Scholar
  8. J. Esparza. Keeping a crowd safe: On the complexity of parameterized verification. In STACS'14, volume 25 of LIPIcs, pages 1-10, 2014. Google Scholar
  9. J. Esparza, P. Ganty, and R. Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, volume 8044 of LNCS, pages 124-140. Springer, 2013. Google Scholar
  10. B. Genest, D. Kuske, and A. Muscholl. On communicating automata with bounded channels. Fundam. Inform., 80(1-3):147-167, 2007. Google Scholar
  11. S. La Torre, P. Madhusudan, and G. Parlato. The language theory of bounded context-switching. In LATIN'10, volume 6034 of LNCS, pages 96-107. Springer, 2010. Google Scholar
  12. S. La Torre, M. Napoli, and G. Parlato. Scope-bounded pushdown languages. In DLT'14, volume 8633 of LNCS, pages 116-128. Springer, 2014. Google Scholar
  13. N. A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers Inc., 1996. Google Scholar
  14. O. Matz, N. Schweikardt, and W. Thomas. The monadic quantifier alternation hierarchy over grids and graphs. Information and Computation, 179(2):356-383, 2002. Google Scholar
  15. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS'05, volume 3440 of LNCS, pages 93-107. Springer, 2005. Google Scholar
  16. W. Thomas. Elements of an automata theory over partial orders. In POMIV'96, volume 29 of DIMACS. AMS, 1996. 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 About DROPS Imprint Privacy Contact