Brzozowski’s and Up-To Algorithms for Must Testing | SpringerLink
Skip to main content
Springer Nature Link
Log in

Brzozowski’s and Up-To Algorithms for Must Testing

  • Conference paper
Programming Languages and Systems (APLAS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8301))

Included in the following conference series:

Abstract

Checking language equivalence (or inclusion) of finite automata is a classical problem in Computer Science, which has recently received a renewed interest and found novel and more effective solutions, such as approaches based on antichains or bisimulations up-to. Several notions of equivalence (or preorder) have been proposed for the analysis of concurrent systems. Usually, the problem of checking these equivalences is reduced to checking bisimilarity. In this paper, we take a different approach and propose to adapt algorithms for language equivalence to check one prime equivalence in concurrency theory, must testing semantics. To achieve this transfer of technology from language to must semantics, we take a coalgebraic outlook at the problem.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  2. Bezhanishvili, N., Kupke, C., Panangaden, P.: Minimization via duality. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 191–205. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Bonchi, F., Bonsangue, M., Caltais, G., Rutten, J., Silva, A.: Final semantics for decorated traces. Elect. Not. in Theor. Comput. Sci. 286, 73–86 (2012)

    Article  MathSciNet  Google Scholar 

  4. Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M., Silva, A.: Brzozowski’s algorithm (Co)Algebraically. In: Constable, R.L., Silva, A. (eds.) Kozen Festschrift. LNCS, vol. 7230, pp. 12–23. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  5. Bonchi, F., Caltais, G., Pous, D., Silva, A.: Brzozowski’s and up-to algorithms for must testing (full version), http://www.alexandrasilva.org/files/brz-hkc-must-full.pdf

  6. Bonchi, F., Caltais, G., Pous, D., Silva, A.: Web appendix of this paper, with implementation of the algorithms (July 2013), http://perso.ens-lyon.fr/damien.pous/brz

  7. Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: POPL, pp. 457–468. ACM (2013)

    Google Scholar 

  8. Boreale, M., Gadducci, F.: Processes as formal power series: a coinductive approach to denotational semantics. TCS 360(1), 440–458 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  9. Brzozowski, J.A.: Canonical regular expressions and minimal state graphs for definite events. Mathematical Theory of Automata 12(6), 529–561 (1962)

    Google Scholar 

  10. Calzolai, F., De Nicola, R., Loreti, M., Tiezzi, F.: TAPAs: A tool for the analysis of process algebras. In: Jensen, K., van der Aalst, W.M.P., Billington, J. (eds.) ToPNoC I. LNCS, vol. 5100, pp. 54–70. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  11. Cancila, D., Honsell, F., Lenisa, M.: Generalized coiteration schemata. Elect. Not. in Theor. Comput. Sci. 82(1) (2003)

    Google Scholar 

  12. Cleaveland, R., Hennessy, M.: Testing equivalence as a bisimulation equivalence. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 11–23. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

  13. Cleaveland, R., Parrow, J., Steffen, B.: The Concurrency Workbench: A semantics-based tool for the verification of concurrent systems. TOPLAS 15(1), 36–72 (1993)

    Article  Google Scholar 

  14. De Nicola, R., Hennessy, M.: Testing equivalences for processes. TCS 34, 83–133 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  15. Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Real-reward testing for probabilistic processes. In: QAPL. EPTCS, vol. 57, pp. 61–73 (2011)

    Google Scholar 

  16. Hopcroft, J.E.: An n log n algorithm for minimizing in a finite automaton. In: Proc. Int. Symp. of Theory of Machines and Computations, pp. 189–196. Academic Press (1971)

    Google Scholar 

  17. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. In: PODC 1983, pp. 228–240. ACM, New York (1983)

    Google Scholar 

  18. Klin, B.: A coalgebraic approach to process equivalence and a coinduction principle for traces. Elect. Not. in Theor. Comput. Sci. 106, 201–218 (2004)

    Article  MathSciNet  Google Scholar 

  19. Klin, B.: Bialgebras for structural operational semantics: An introduction. TCS 412(38), 5043–5069 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  20. Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. Elect. Not. in Theor. Comput. Sci. 19, 2–22 (1999)

    Article  MathSciNet  Google Scholar 

  21. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

    Google Scholar 

  22. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  23. Parrow, J., Sjödin, P.: Designing a multiway synchronization protocol. Computer Communications 19(14), 1151–1160 (1996)

    Article  Google Scholar 

  24. Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  25. Rot, J., Bonsangue, M., Rutten, J.: Coalgebraic bisimulation-up-to. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 369–381. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  26. Rutten, J.: Universal coalgebra: a theory of systems. TCS 249(1), 3–80 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  27. Sangiorgi, D.: On the bisimulation proof method. Math. Struc. in CS 8, 447–479 (1998)

    MathSciNet  MATH  Google Scholar 

  28. Silva, A., Bonchi, F., Bonsangue, M., Rutten, J.: Generalizing the powerset construction, coalgebraically. In: Proc. FSTTCS. LIPIcs, vol. 8, pp. 272–283 (2010)

    Google Scholar 

  29. Tabakov, D., Vardi, M.: Experimental evaluation of classical automata constructions. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol. 3835, pp. 396–411. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  30. van Glabbeek, R.: The linear time - branching time spectrum I. The semantics of concrete, sequential processes. In: Handbook of Process Algebra, pp. 3–99. Elsevier (2001)

    Google Scholar 

  31. Watson, B.W.: Taxonomies and Toolkits of Regular Language Algorithms. PhD thesis, Eindhoven University of Technology, the Netherlands (1995)

    Google Scholar 

  32. De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, UCBL, ENS Lyon, U. de Lyon, CNRS, France

    Filippo Bonchi & Damien Pous

  2. Reykjavik University, Iceland

    Georgiana Caltais

  3. Radboud University Nijmegen, Netherlands

    Alexandra Silva

Authors
  1. Filippo Bonchi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georgiana Caltais
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Damien Pous
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alexandra Silva
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indiana University, 150 S. Woodlawn Avenue, 47405-7104, Bloomington, IN, USA

    Chung-chieh Shan

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer International Publishing Switzerland

About this paper

Cite this paper

Bonchi, F., Caltais, G., Pous, D., Silva, A. (2013). Brzozowski’s and Up-To Algorithms for Must Testing. In: Shan, Cc. (eds) Programming Languages and Systems. APLAS 2013. Lecture Notes in Computer Science, vol 8301. Springer, Cham. https://doi.org/10.1007/978-3-319-03542-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-03542-0_1

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-03541-3

  • Online ISBN: 978-3-319-03542-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics