Skip to main content
SpringerLink
Log in

Alternating Parity Krivine Automata

  • Conference paper
Book cover Mathematical Foundations of Computer Science 2014 (MFCS 2014)

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

Abstract

Higher-Order Modal Fixpoint Logic HFL is a non-regular extension of the modal μ-calculus by a typed λ-calculus. The model-checking problem for this logic is decidable over finite structures. We present an automaton model that captures the semantics of HFL. This automaton model combines alternating parity automata with the lookup mechanisms from the Krivine machine.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Transactions of the American Mathematical Society 141, 1–35 (1969)

    MATH  MathSciNet  Google Scholar 

  2. Büchi, J.R.: Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly 6(1-6), 66–92 (1960)

    Article  MATH  Google Scholar 

  3. Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312–360 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  4. Lange, M., Lozes, É., Guzmán, M.V.: Model-checking process equivalences. In: Faella, M., Murano, A. (eds.) GandALF. EPTCS, vol. 96, pp. 43–56 (2012)

    Google Scholar 

  5. Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC, pp. 202–211. ACM (2004)

    Google Scholar 

  6. Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)

    Google Scholar 

  7. Müller-Olm, M.: A modal fixpoint logic with chop. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 510–520. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Viswanathan, M., Viswanathan, R.: A higher order modal fixed point logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 512–528. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Axelsson, R., Lange, M., Somla, R.: The complexity of model checking higher-order fixpoint logic. Logical Methods in Computer Science 3(2) (2007)

    Google Scholar 

  10. Axelsson, R., Hague, M., Kreutzer, S., Lange, M., Latte, M.: Extended computation tree logic. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 67–81. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Krivine, J.L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3), 199–207 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  12. Salvati, S., Walukiewicz, I.: Krivine machines and higher-order schemes. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) ICALP 2011, Part II. LNCS, vol. 6756, pp. 162–173. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  13. Lange, M.: The alternation hierarchy in fixpoint logic with chop is strict too. Inf. Comput. 204(9), 1346–1367 (2006)

    Article  MATH  Google Scholar 

  14. Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput. 164(2), 234–263 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  15. Bradfield, J.C.: The modal mu-calculus alternation hierarchy is strict. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 233–246. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  16. Carayol, A., Serre, O.: Collapsible pushdown automata and labeled recursion schemes: Equivalence, safety and effective selection. In: LICS, pp. 165–174. IEEE (2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Elektrotechnik und Informatik, Universität Kassel, Wilhelmshöher Allee 73, 34121, Kassel, Germany

    Florian Bruse

Authors
  1. Florian Bruse
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Eötvös Loránd University, Pázmány Péter sétány 1/C, 1117, Budapest, Hungary

    Erzsébet Csuhaj-Varjú

  2. Fakultät für Informatik und Automatisierung, Technische Universität Ilmenau, Helmholtzplatz, 598693, Ilmenau, Germany

    Martin Dietzfelbinger

  3. Institute of Informatics, Szeged University, Tisza Lajos krt. 103, 6720, Szeged, Hungary

    Zoltán Ésik

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer-Verlag GmbH Berlin Heidelberg

About this paper

Cite this paper

Bruse, F. (2014). Alternating Parity Krivine Automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds) Mathematical Foundations of Computer Science 2014. MFCS 2014. Lecture Notes in Computer Science, vol 8634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44522-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-44522-8_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-44521-1

  • Online ISBN: 978-3-662-44522-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation