[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Enhancing Simulation for Checking Language Containment

  • Conference paper
Theory and Applications of Models of Computation (TAMC 2007)

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

  • 1190 Accesses

Abstract

Many verification approaches based on automata theory are related to the language containment problem, which is PSPACE-complete for nondeterministic automata. To avoid such a complexity, one may use simulation as an approximation to language containment, since simulation implies language containment and computing simulation is a polynomial time problem. As it is an approximation, there exists a gap between simulation and language containment, therefore there has been an effort to develop methods to narrow the gap while keeping the computation in polynomial time. In this paper, we present such an approach by building a Büchi  automaton based on partial marked subset construction to be used in the computation of simulation relation, such that the automaton preserves the original language and has a structure that helps identify more pairs of automata that are in language containment relation. This approach is an improvement to the fair-k-simulation method [3].

Supported by the National Natural Science Foundation of China under Grant No. 60573012 and 60421001, and the National Grand Fundamental Research 973 Program of China under Grant No. 2002cb312200.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Bustan, D., Grumberg, O.: Applicability of fair simulation. Information and computation 194(1), 1–18 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  2. Dill, D.L., Hu, A.J., Wong-Toi, H.: Checking for language inclusion using simulation preorders. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 255–265. Springer, Heidelberg (1992)

    Google Scholar 

  3. Etessami, K.: A Hierarchy of Polynomial-Time Computable Simulations for Automata. In: Brim, L., et al. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 131–144. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  4. Holzmann, G.J., Etessami, K.: Optimizing Büchi Automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 153–167. Springer, Heidelberg (2000)

    Google Scholar 

  5. Etessami, K., Wilke, T., Schuller, R.: Fair simulation relations, parity games, and state space reduction for Büchi automata. SIAM Journal of Computing 34(5), 1159–1175 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  6. Fritz, C.: Constructing Büchi Automata from Linear Temporal Logic Using Simulation Relations for Alternating Büchi Automata. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 35–48. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Gurumurthy, S., Bloem, R., Somenzi, F.: Fair Simulation Minimization. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 610–624. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Gurumurthy, S., et al.: On Complementing Nondeterministic Büchi Automata. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 96–110. Springer, Heidelberg (2003)

    Google Scholar 

  9. Henzinger, T.A., Kupferman, O., Rajamani, S.K.: Fair simulation. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 273–287. Springer, Heidelberg (1997)

    Google Scholar 

  10. Jurdzinski, M.: Small progress measures for solving parity games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  11. Kesten, Y., Piterman, N., Pnueli, A.: Bridging the Gap Between Fair Simulation and Trace Inclusion. Information and Computation 200(1), 35–61 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  12. Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. In: STOC’98, pp. 408–429 (1998)

    Google Scholar 

  13. Lindahl, A.: Complementation of Büchi automata: A survey and implementation. Master thesis, Linköpings university Department of computer and information science (2004)

    Google Scholar 

  14. Miyano, S., Hayashi, T.: Alternating Finite Automata on ω-Words. Theoretical Computer Science 32, 321–330 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  15. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  16. Mukund, M.: Finite-state Automata on Infinte Inputs. In: Sixth National Seminar on Theoretical Computer Science, Banasthali Vidyapith, Banasthali, Rajasthan (1996)

    Google Scholar 

  17. Rabin, M.O., Scott, D.: Finite automata and their decision problems. IBM Journal of Research 3(2), 115–125 (1959)

    MathSciNet  Google Scholar 

  18. Safra, S.: Complexity of automata on infinite object. PhD thesis (1989)

    Google Scholar 

  19. Somenzi, F., Bloem, R.: Efficient Büchi automata from LTL formulae. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 248–263. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China

    Jin Yi & Wenhui Zhang

  2. Graduate University of the Chinese Academy of Sciences, Beijing, China

    Jin Yi

Authors
  1. Jin Yi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wenhui Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jin-Yi Cai S. Barry Cooper Hong Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Yi, J., Zhang, W. (2007). Enhancing Simulation for Checking Language Containment. In: Cai, JY., Cooper, S.B., Zhu, H. (eds) Theory and Applications of Models of Computation. TAMC 2007. Lecture Notes in Computer Science, vol 4484. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72504-6_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-72504-6_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-72503-9

  • Online ISBN: 978-3-540-72504-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation