Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 2006: Computer Science Logic pp 31–40Cite as

Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract)

  • Conference paper

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

Abstract

We present some results on a game-semantic approach to verifying infinite structures that are generated by higher-order recursion schemes. The key idea is a certain Transference Principle from the structure generated by a given recursion scheme to an auxiliary computation tree, which is itself generated by a related order-0 recursion scheme. By a structural analysis of the computation tree based on the innocent game semantics of the recursion scheme, we can infer certain properties of the generated structure by appropriate algorithmic analysis of the computation tree.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about 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. Trans. Amer. Maths. Soc. 141, 1–35 (1969)

    Article  MATH  MathSciNet  Google Scholar 

  2. Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science 37, 51–75 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  3. Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol. 1099, pp. 194–205. Springer, Heidelberg (1996)

    Google Scholar 

  4. Stirling, C.: Decidability of bisimulation equivalence for pushdown processes (2000) (submitted for publication)

    Google Scholar 

  5. Knapik, T., Niwiński, D., Urzyczyn, P.: Higher-order pushdown trees are easy. In: Nielsen, M., Engberg, U. (eds.) FOSSACS 2002. LNCS, vol. 2303, pp. 205–222. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Caucal, D.: On infinite terms having a decidable monadic theory. In: Diks, K., Rytter, W. (eds.) MFCS 2002. LNCS, vol. 2420, pp. 165–176. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  7. Aehlig, K., de Miranda, J.G., Ong, C.H.L.: The monadic second order theory of trees given by arbitrary level two recursion schemes is decidable. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 39–54. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Knapik, T., Niwiński, D., Urzyczyn, P., Walukiewicz, I.: Unsafe grammars and panic automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1450–1461. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  9. Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional mu-calculus with respect to msol. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)

    Google Scholar 

  10. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes, 42 pages (preprint, 2006)

    Google Scholar 

  11. Ong, C.H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of IEEE Symposium on Logic in Computer Science. Computer Society Press (2006)

    Google Scholar 

  12. Hyland, J.M.E., Ong, C.H.L.: On Full Abstraction for PCF: I. Models, observables and the full abstraction problem, II. Dialogue games and innocent strategies, III. A fully abstract and universal game model. Information and Computation 163, 285–408 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  13. Ong, C.H.L.: Local computation of beta-reduction by game semantics (preprint, 2006)

    Google Scholar 

  14. Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proceedings of FOCS 1991, pp. 368–377 (1991)

    Google Scholar 

  15. Engelfriet, J.: Interated stack automata and complexity classes. Information and Computation, 21–75 (1991)

    Google Scholar 

  16. Cachat, T.: Higher order pushdown automata, the Caucal hierarchy of graphs and parity games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 556–569. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. Murawski, A.S., Ong, C.H.L.: Collapsible pushdown automata and recursion schemes (preprint, 2006)

    Google Scholar 

  18. Aehlig, K., de Miranda, J.G., Ong, C.H.L.: Safety is not a restriction at level 2 for string languages. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 490–501. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Aehlig, K.: A finite semantics for simply-typed lambda terms for infinite runs of automata. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Oxford University Computing Laboratory,  

    C. -H. L. Ong

Authors
  1. C. -H. L. Ong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Group on Mathematical Linguistics, Rovira i Virgili University, Tarragona, Spain

    Zoltán Ésik

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ong, C.H.L. (2006). Some Results on a Game-Semantic Approach to Verifying Finitely-Presentable Infinite Structures (Extended Abstract). In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_2

Download citation

  • DOI: https://doi.org/10.1007/11874683_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-45458-8

  • Online ISBN: 978-3-540-45459-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation