Reachability Problems on Partially Lossy Queue Automata | SpringerLink
Skip to main content
Springer Nature Link
Log in

Reachability Problems on Partially Lossy Queue Automata

  • Conference paper
  • First Online:
Reachability Problems (RP 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11674))

Included in the following conference series:

Abstract

We study the reachability problem for queue automata and lossy queue automata. Concretely, we consider the set of queue contents which are forwards resp. backwards reachable from a given set of queue contents. Here, we prove the preservation of regularity if the queue automaton loops through some special sets of transformations. This is a generalization of the results by Boigelot et al. and Abdulla et al. regarding queue automata looping through a single sequence of transformations. We also prove that our construction is effective and efficient.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91–101 (1996). https://doi.org/10.1006/inco.1996.0053

    Article  MathSciNet  MATH  Google Scholar 

  2. Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des. 25(1), 39–65 (2004). https://doi.org/10.1023/B:FORM.0000033962.51898.1a

    Article  MATH  Google Scholar 

  3. Boigelot, B., Godefroid, P.: Symbolic verification of communication protocols with infinite state spaces using QDDs. Formal Methods Syst. Des. 14(3), 237–255 (1999). https://doi.org/10.1023/A:1008719024240

    Article  Google Scholar 

  4. Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs (extended abstract). In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol. 1302, pp. 172–186. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0032741

    Chapter  Google Scholar 

  5. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63141-0_10

    Chapter  Google Scholar 

  6. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983). https://doi.org/10.1145/322374.322380

    Article  MathSciNet  MATH  Google Scholar 

  7. Chambart, P., Schnoebelen, P.: The ordinal recursive complexity of lossy channel systems. In: LICS 2008, pp. 205–216. IEEE Computer Society Press (2008). https://doi.org/10.1109/LICS.2008.47

  8. Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_20

    Chapter  Google Scholar 

  9. Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9, 27–37 (1997). https://doi.org/10.1016/S1571-0661(05)80426-8

    Article  MATH  Google Scholar 

  10. Haines, L.H.: On free monoids partially ordered by embedding. J. Comb. Theory 6(1), 94–98 (1969). https://doi.org/10.1016/S0021-9800(69)80111-0

    Article  MathSciNet  MATH  Google Scholar 

  11. Huschenbett, M., Kuske, D., Zetzsche, G.: The monoid of queue actions. Semigroup Forum 95(3), 475–508 (2017). https://doi.org/10.1007/s00233-016-9835-4

    Article  MathSciNet  MATH  Google Scholar 

  12. Köcher, C.: Rational, recognizable, and aperiodic sets in the partially lossy queue monoid. In: STACS 2018. LIPIcs, vol. 96, pp. 45:1–45:14. Dagstuhl Publishing (2018). https://doi.org/10.4230/LIPIcs.STACS.2018.45

  13. Köcher, C., Kuske, D., Prianychnykova, O.: The inclusion structure of partially lossy queue monoids and their trace submonoids. RAIRO - Theor. Inf. Appl. 52(1), 55–86 (2018). https://doi.org/10.1051/ita/2018003

    Article  MathSciNet  MATH  Google Scholar 

  14. Mayr, R.: Undecidable problems in unreliable computations. Theoret. Comput. Sci. 297(1), 337–354 (2003). https://doi.org/10.1016/S0304-3975(02)00646-1

    Article  MathSciNet  MATH  Google Scholar 

  15. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251–261 (2002). https://doi.org/10.1016/S0020-0190(01)00337-4

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgment

The author would like to thank Dietrich Kuske and the anonymous reviewers of this paper for their helpful suggestions to improve this paper.

Author information

Authors and Affiliations

  1. Automata and Logics Group, Technische Universität Ilmenau, Ilmenau, Germany

    Chris Köcher

Authors
  1. Chris Köcher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Chris Köcher .

Editor information

Editors and Affiliations

  1. Université Libre de Bruxelles, Brussels, Belgium

    Emmanuel Filiot

  2. Université Catholique de Louvain, Louvain-la-Neuve, Belgium

    Raphaël Jungers

  3. University of Liverpool, Liverpool, UK

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Köcher, C. (2019). Reachability Problems on Partially Lossy Queue Automata. In: Filiot, E., Jungers, R., Potapov, I. (eds) Reachability Problems. RP 2019. Lecture Notes in Computer Science(), vol 11674. Springer, Cham. https://doi.org/10.1007/978-3-030-30806-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30806-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30805-6

  • Online ISBN: 978-3-030-30806-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation